In the new CI script, enable build of runtime with debugging support

This is done by passing the -with-debug-runtime option to the configure
script on the non-Windows systems.

On Windows, a sed invocation is used to set RUNTIMED to true in
config/Makefile.
master
Sébastien Hinderer 2017-04-14 18:45:56 +02:00
parent d847e077e8
commit fdc63806c3
1 changed files with 5 additions and 1 deletions

View File

@ -169,11 +169,15 @@ $make distclean || :
git clean -f -d -x
case $configure in
unix) eval "./configure -prefix '$instdir' $confoptions";;
unix)
confoptions="$confoptions -with-debug-runtime"
eval "./configure -prefix '$instdir' $confoptions"
;;
nt)
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%RUNTIMED=.\+%RUNTIMED=true%' config/Makefile
;;
*) error "internal error";;
esac