From dde2f370546e03a1e2a85b11162c20aadd80b87f Mon Sep 17 00:00:00 2001
From: Nico Schottelius <nico@kr.ethz.ch>
Date: Tue, 29 Mar 2011 16:51:11 +0200
Subject: [PATCH] make build.sh die on error

Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>
---
 build.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/build.sh b/build.sh
index 335bbe9c..52b3466e 100755
--- a/build.sh
+++ b/build.sh
@@ -23,6 +23,9 @@
 # Pull a directory from a target, both sides have the same name (i.e. explorers)
 #
 
+# exit on any error
+set -e
+
 # Manpage and HTML
 A2XM="a2x -f manpage --no-xmllint"
 A2XH="a2x -f xhtml --no-xmllint"