Generate shebang header at make world stage. #42
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Ken,
while making mosml RPM package for my distribution I met a problem with incorrect shebang line in binaries, that were created with installed MosML.
Packages are built under regular user, so, one can not write to system directories. The packaging process involves 2 stages - build and install. On build stage you can use any directory as PREFIX, while on install stage PREFIX is provided by RPM build system, so it is a fake root, smth like
/home/const/tmp/mosml-buildroot
Therefore shebang header should be generated at build stage, but not at install stage. And overall, no path variable should be defined at install stage.
This header does not affect bootstrap compilers, because these binaries do not include shebang header and should be run with direct call to camlrunm. You can check it by (as I did):
make world
src/compiler
directory,make clean
,make
,make promote