diff options
| author | Sébastien Hinderer <Sebastien.Hinderer@inria.fr> | 2017-04-14 18:45:56 +0200 |
|---|---|---|
| committer | Sébastien Hinderer <Sebastien.Hinderer@inria.fr> | 2017-04-14 18:53:34 +0200 |
| commit | fdc63806c3c243267e3e82207971794bdd4128ca (patch) | |
| tree | d6c4e1b3a4e61f5e95bebac68271e74121fca063 /tools | |
| parent | d847e077e8d9f5f434e630c05977b8657de5a57d (diff) | |
| download | ocaml-fdc63806c3c243267e3e82207971794bdd4128ca.tar.gz | |
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.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci-build-new | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/ci-build-new b/tools/ci-build-new index 3adb56212a..40a6f120b7 100755 --- a/tools/ci-build-new +++ b/tools/ci-build-new @@ -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 |