Let configure.sh change Makefile
With a few additional lines, one can let configure.sh write the environment variables to the Makefile, such that it doesn't need to be sourced any more and therefore won't change the environment of the user.
With a few additional lines, one can let configure.sh write the environment variables to the Makefile, such that it doesn't need to be sourced any more and therefore won't change the environment of the user.