diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-19 17:13:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-05 17:11:59 +0200 |
| commit | 4e7d1a239fe325ca938db6144f77cdabd974ac17 (patch) | |
| tree | 01b49a251c2664a4c9d13010c95e1529e68c3029 /dev/build | |
| parent | df6ae3d59af8f880a0411217b8e6f0dae0b92133 (diff) | |
In regression test mode, run cygwin setup to install dependencies.
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/MakeCoq_MinGW.bat | 3 |
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% ^ |