aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index aa05051..e91aa17 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -110,6 +110,7 @@ make-coq-latest:
- coqc --version
- git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci
- cd /home/coq/ci
+ - git rev-parse --verify HEAD
except:
- tags
- merge_requests