diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/MakeCoq_MinGW.bat | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c75acb0560..577ce35aae 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -420,6 +420,7 @@ copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOT ECHO ========== BUILD COQ ==========
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
|