Missing stuff in gitlab-ci

2019-05-15 16:35:46 +02:00 · 2019-05-15 16:35:46 +02:00 · 834cc8c072
commit 834cc8c072
parent c60329ef78
1 changed files with 1 additions and 1 deletions
--- 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: