don't check test output on coq.dev (it's broken due to a Coq bug)

1342eb50 · Ralf Jung · dba6f901 · 1342eb50 · 16c8b610 · 99c935d2
Commit 1342eb50 authored May 17, 2018 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

.gitlab-ci.yml .gitlab-ci.yml +1 -0

ci ci +1 -1

No files found.
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -29,6 +29,7 @@ variables:
 build-coq.dev:
  <<: *template
  variables:
+    BUILD_TARGET: "ref" # don't check test output
    OPAM_PINS: "coq version dev"
    VALIDATE: "1"


--- a/ci @ 16c8b610
+++ b/ci @ 16c8b610
-Subproject commit 99c935d2007358fe4028560e96f9c136e608e696
+Subproject commit 16c8b6107119db3448b6828d3d2757888f2b2376