From 6d0aec5ab0675c579aa43727c715555b89038749 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Fri, 16 Sep 2016 14:23:32 +0200
Subject: [PATCH] Disable make quick in CI

---
 .gitlab-ci.yml | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1bafef34..948fdb8f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -21,23 +21,23 @@ iris:
   only:
   - master
 
-vio:
-  stage: quickbuild
-  tags:
-  - coq
-  script: >
-    cd coq/ra/;
-    coqc -v;
-    time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
-    cat build-log-vio.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
-  only:
-  - master
-  cache:
-    paths:
-    - coq/ra/*.vio
-  artifacts:
-    paths:
-    - coq/ra/build-time-vio.txt
+# vio:
+#   stage: quickbuild
+#   tags:
+#   - coq
+#   script: >
+#     cd coq/ra/;
+#     coqc -v;
+#     time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
+#     cat build-log-vio.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
+#   only:
+#   - master
+#   cache:
+#     paths:
+#     - coq/ra/*.vio
+#   artifacts:
+#     paths:
+#     - coq/ra/build-time-vio.txt
 
 # vio2vo:
 #   stage: quickcheck
-- 
GitLab