tools/ci-build: honor instdir on non-configure builds

The instdir environment variable is used by ci-build to define where
make install should install the compiler. Before this commit, a value was
assigned to instdir for the Windows builds that do not use configure,
but then this value was not taken into account, making the assignments useless
for those builds that do not use configure.

This commit fixes this by using instdir to override the value of PREFIX
in config/Makefile.
master
Sébastien Hinderer 2017-04-26 11:41:36 +02:00
parent 1918a6fed2
commit 023f3e3fa2
1 changed files with 1 additions and 0 deletions

View File

@ -182,6 +182,7 @@ case $configure in
cp config/m-nt.h config/m.h
cp config/s-nt.h config/s.h
cp config/Makefile.${OCAML_ARCH} config/Makefile
sed -i "s%PREFIX=\(.\+\)%PREFIX=${instdir}%" config/Makefile
sed -i 's%RUNTIMED=.\+%RUNTIMED=true%' config/Makefile
if $flambda; then
sed -i 's%FLAMBDA=.\+%FLAMBDA=true%' config/Makefile