From 58208b41a61c2a9ed98c167e05fb069c68602966 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Fri, 14 Dec 2018 18:26:26 +0100
Subject: Fix issue: Windows CI: cygwin install cache is not reused #9212

---
 dev/ci/gitlab.bat | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 386a3de204..635804687a 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -26,12 +26,12 @@ if %ARCH% == 64 (
 
 SET CYGROOT=C:\ci\cygwin%ARCH%
 SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
 
 CALL :MakeUniqueFolder %CYGROOT% CYGROOT
 CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
 
 powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
 SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
 SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
 SET COQREGTESTING=Y
-- 
cgit v1.2.3