From 834cc8c0724b01ee9bcf6e417979692f4261d5e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Wed, 15 May 2019 16:35:46 +0200 Subject: [PATCH] Missing stuff in gitlab-ci --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e5147cb4e..9bba02f83 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -42,7 +42,7 @@ local-dune-job: - (dune build -p ligo) # TODO: also try instead from time to time: #- (cd ./src/; dune build -p ligo) - dune build -p ligo + - dune build @ligo-test local-repo-job: script: