From e358e641068ee2947ba6736b06138284f98c2101 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20M=C3=B6bius?= <moebius@cs.rwth-aachen.de>
Date: Wed, 25 Nov 2015 12:00:41 +0100
Subject: [PATCH] Exit build scripts on any error

---
 CI/ci-linux.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CI/ci-linux.sh b/CI/ci-linux.sh
index 30a08372..84455a33 100755
--- a/CI/ci-linux.sh
+++ b/CI/ci-linux.sh
@@ -3,6 +3,9 @@
 COMPILER=$1
 LANGUAGE=$2
 
+# Exit script on any error
+set -e 
+
 OPTIONS=""
 
 if [ "$COMPILER" == "gcc" ]; then