From 73a21e03e1d3a34a212a98b80ec979d3fd7c07d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=BCthing?=
<steffen.muething@iwr.uni-heidelberg.de>
Date: Wed, 4 Jul 2018 12:50:58 +0200
Subject: [PATCH] Install required module dune-opcounter
---
.gitlab-ci.yml | 1 +
1 file changed, 1 insertion(+)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2e6b48db..40e860ff 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,6 +5,7 @@ variables:
before_script:
- echo "Running make concurrently with ${DUNECI_PARALLEL} cores, where possibly"
- patches/apply_patches.sh
+ - duneci-install-module --recursive https://gitlab.dune-project.org/dominic/dune-opcounter.git
git-debian-10-gcc-7-14:
image: "registry.dune-project.org/docker/ci/dune-pdelab:git-debian-10-gcc-7-14"
--
GitLab