From 2b27b8880254420f1630d8d40442d72c0e2255c2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 21 Nov 2018 11:36:38 +0100
Subject: [Windows CI] Do not build any addon if WINDOWS is not
 enabled_all_addons.

Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
---
 dev/ci/gitlab.bat | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev/ci/gitlab.bat')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 918d289ae2..386a3de204 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -39,6 +39,10 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\
 
 IF "%WINDOWS%" == "enabled_all_addons" (
   SET EXTRA_ADDONS=^
+    -addon=bignums ^
+    -addon=equations ^
+    -addon=ltac2 ^
+    -addon=mtac2 ^
     -addon=mathcomp ^
     -addon=menhir ^
     -addon=menhirlib ^
@@ -56,10 +60,6 @@ IF "%WINDOWS%" == "enabled_all_addons" (
 call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
   -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
   -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-  -addon=bignums ^
-  -addon=equations ^
-  -addon=ltac2 ^
-  -addon=mtac2 ^
   %EXTRA_ADDONS% ^
   -make=N ^
   -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-- 
cgit v1.2.3