try to tell gitlab CI what to do (f391510d) · Commits · Iris / Iris · GitLab

Snippets Groups Projects

There was a problem fetching the pipeline metadata.

Commit f391510d authored 9 years ago by Ralf Jung

try to tell gitlab CI what to do

parent ead5cad9

No related branches found

No related tags found

No related merge requests found

Pipeline #

Hide whitespace changes

Inline Side-by-side

Showing with 7 additions and 0 deletions

0 → 100644

+ 7

− 0

View file @ f391510d

 image: coq:8.5
 buildjob:
   tags:
   - coq
   script:
   - make

Please register or to comment