From 9511efb2ba909ec9d198d02bedf4074d41500474 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Sat, 18 Jan 2020 15:59:13 +0100
Subject: Clear patches folder before each windows build run

---
 dev/build/windows/MakeCoq_MinGW.bat | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

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
-- 
cgit v1.2.3