From 31db700ad4cf0fda78dffa6703f86400d86318c5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 30 May 2018 18:15:59 +0200
Subject: Gitlab: retry failed "build" jobs once

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4784f0db0..947532cea 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -50,6 +50,7 @@ before_script:
 # TODO figure out how to build doc for installed Coq
 .build-template: &build-template
   stage: build
+  retry: 1
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
-- 
cgit v1.2.3