From 39d3e313614d33b353978847f8d00d3fa2f2428f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Sep 2020 17:49:43 +0200
Subject: fix

---
 .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 173d42d..3f8309a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -128,6 +128,7 @@ coq-dev:
     - git rev-parse --verify HEAD
     - git describe --all --long --abbrev=40 --always --dirty
     - pwd
+  script:
     - cd mathcomp
     - make test-suite
   except:
-- 
cgit v1.2.3