Inria CI: add -no-shared-libs to script

This option was specified in the Cygwin64 slave's configuration, but this
makes it impossible to use different values on differnet branches,
which is needed when switching to autoconf.
master
Sébastien Hinderer 2018-12-21 11:01:14 +01:00
parent e8d4324ee6
commit 0723ac158e
1 changed files with 1 additions and 0 deletions

View File

@ -128,6 +128,7 @@ case "${OCAML_ARCH}" in
cleanup=true
check_make_alldepend=true
dorebase=true
confoptions="$confoptions -no-shared-libs "
;;
mingw)
instdir='C:/ocamlmgw'