To facilitate running make in the build configuration directory, we create a Makefile out of a template. Unfortunately, this references the real Makefile at $TOPDIR instead of $WORKSPACE_ROOT. They are normally equivalent, but if you are using custom additions, they might not be.