From 286a9397b8c367f08a350a18826e7ab603775e91 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Hinderer?= <Sebastien.Hinderer@inria.fr>
Date: Wed, 25 Nov 2020 10:50:11 +0100
Subject: [PATCH] Inria CI fix

The step-by-step-build job should stop on errors
---
 tools/ci/inria/step-by-step-build/script | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/ci/inria/step-by-step-build/script b/tools/ci/inria/step-by-step-build/script
index 8397e6836..a394d612d 100755
--- a/tools/ci/inria/step-by-step-build/script
+++ b/tools/ci/inria/step-by-step-build/script
@@ -14,6 +14,9 @@
 #*                                                                        *
 #**************************************************************************
 
+# Be verbose and stop on errors
+set -ex
+
 jobs=-j8
 instdir="$HOME/ocaml-tmp-install-$$"
 ./configure --prefix "$instdir" --disable-dependency-generation