From 7ab1656e0ff764175a52af417ec02a3feaf0a328 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Hinderer?= Date: Wed, 13 Dec 2017 15:08:04 +0100 Subject: [PATCH] tools/ci-build-other-configs should stop on errors --- tools/ci-build-other-configs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tools/ci-build-other-configs b/tools/ci-build-other-configs index ac6558151..5cc7ab18b 100755 --- a/tools/ci-build-other-configs +++ b/tools/ci-build-other-configs @@ -16,6 +16,9 @@ # Commands to run for the 'other-configs' job on Inria's CI +# Stop on error +set -e + ./tools/ci-build -conf -no-native-compiler -no-native ./tools/ci-build -conf -no-naked-pointers ./tools/ci-build -conf -flambda -conf -no-naked-pointers