diff options
| author | Gaëtan Gilbert | 2021-02-16 13:05:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-16 13:07:14 +0100 |
| commit | 43ed1525126723858e6e3cbd63f26dc2af479511 (patch) | |
| tree | d2e6b323d69fbed638d5a26119959903183bea85 /.gitlab-ci.yml | |
| parent | c0e0e637c61e075f43b73d1ddd8eaa9d79b27561 (diff) | |
Only run windows job when WINDOWS=enabled
This seems to have been missed in
https://github.com/coq/coq/pull/13598
(16cd0d5cfc0c4702b8220dad8e91f31a89d904ba)
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 3 insertions, 0 deletions
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 |