From f391510db4182d5f77a16d2ead8130587d29142c Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 22 Feb 2016 16:26:31 +0100 Subject: [PATCH] try to tell gitlab CI what to do --- .gitlab-ci.yml | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 .gitlab-ci.yml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml new file mode 100644 index 000000000..f890f4615 --- /dev/null +++ b/.gitlab-ci.yml @@ -0,0 +1,7 @@ +image: coq:8.5 + +buildjob: + tags: + - coq + script: + - make -- GitLab