From 15287c3b127667337601088a203545a252a25efb Mon Sep 17 00:00:00 2001 From: David Allsopp Date: Wed, 14 Mar 2018 16:18:56 +0100 Subject: [PATCH] Use --with-private-runtime on AppVeyor --- appveyor_build.cmd | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/appveyor_build.cmd b/appveyor_build.cmd index f6dc81ac3fe..2e844905212 100644 --- a/appveyor_build.cmd +++ b/appveyor_build.cmd @@ -154,7 +154,9 @@ if "%OCAML_PORT%" equ "" ( ) set LIB_EXT= if "%DEP_MODE%" equ "lib-ext" set LIB_EXT=^&^& make lib-ext -"%CYG_ROOT%\bin\bash.exe" -lc "cd $APPVEYOR_BUILD_FOLDER %LIB_PKG% && ./configure %LIB_EXT% && make opam %POST_COMMAND%" || exit /b 1 +set PRIVATE_RUNTIME= +if "%OCAML_PORT:~0,5%" equ "mingw" set PRIVATE_RUNTIME=--with-private-runtime +"%CYG_ROOT%\bin\bash.exe" -lc "cd $APPVEYOR_BUILD_FOLDER %LIB_PKG% && ./configure %PRIVATE_RUNTIME% %LIB_EXT% && make opam %POST_COMMAND%" || exit /b 1 goto :EOF :test