From 633b462dc0c0211d353faebc6acbe6393c1566b6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Apr 2020 11:16:28 +0200
Subject: CI: Ignore spurious errors in validate jobs

---
 .gitlab-ci.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8880ec1d21..f439b0c34f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -212,7 +212,10 @@ before_script:
   dependencies:
     - not-a-real-job
   script:
-    - cd _install_ci
+    # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
+    # the validate:quick job is sometimes started before build:quick, without artifacts
+    # we ignore these spurious errors so if the job fails it's a real error
+    - cd _install_ci || exit 0
     - find lib/coq/ -name '*.vo' -fprint0 vofiles
     - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
     - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
-- 
cgit v1.2.3