diff options
| -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% ^ |