From dca5f08ef5eb96ad08cae7909037f3a52396927d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Feb 2018 16:34:59 +0100
Subject: [PATCH] Step being verbose when the CI preparation script is done

---
 build/opam-ci.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index b6925ba58..bc51df87e 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -63,5 +63,6 @@ echo "[opam-ci] Installing build-dependencies"
 make build-dep OPAMFLAGS=-y
 
 # done
+set +x
 echo
 coqc -v
-- 
GitLab