aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-19 17:13:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-05 17:11:59 +0200
commit4e7d1a239fe325ca938db6144f77cdabd974ac17 (patch)
tree01b49a251c2664a4c9d13010c95e1529e68c3029
parentdf6ae3d59af8f880a0411217b8e6f0dae0b92133 (diff)
In regression test mode, run cygwin setup to install dependencies.
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat3
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index b2efe2ddd..a420b5d8b 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -344,6 +344,9 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
IF NOT "%CYGWIN_QUIET%" == "Y" (
SET RUNSETUP=Y
)
+IF "%COQREGTESTING%" == "Y" (
+ SET RUNSETUP=Y
+)
IF "%RUNSETUP%"=="Y" (
%SETUP% ^