From 43ed1525126723858e6e3cbd63f26dc2af479511 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 16 Feb 2021 13:05:31 +0100
Subject: Only run windows job when WINDOWS=enabled

This seems to have been missed in
https://github.com/coq/coq/pull/13598
(16cd0d5cfc0c4702b8220dad8e91f31a89d904ba)
---
 .gitlab-ci.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 10ec39da12..6a8217674a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -351,6 +351,9 @@ windows64:
     - call dev/ci/platform-windows.bat
   tags:
     - windows-inria
+  only:
+    variables:
+      - $WINDOWS =~ /enabled/
 
 lint:
   stage: stage-1
-- 
cgit v1.2.3