From d5f1c2622661a31e1675474769a2838b5f943f65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Sun, 30 Sep 2018 22:21:01 +0200
Subject: [PATCH] Added another safety option to bash, moved bash invocation to
 a separate file

---
 Makefile           | 3 ++-
 utils/safe-bash.sh | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100755 utils/safe-bash.sh

diff --git a/Makefile b/Makefile
index dd04dce..a102ae2 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,8 @@ COMMIT_TIMESTAMP_ISO_8601 = $$(git log -1 --pretty=format:%ad --date=iso8601-str
 ####################################
 
 MAKEFLAGS = --warn-undefined-variables
-SHELL = bash -euET -o pipefail -c
+SHELL = ${CURDIR}/utils/safe-bash.sh
+# utils/safe-bash.sh
 .SECONDEXPANSION:
 
 Makefiles = Makefile Makefile.example-os Makefile.test-example-os
diff --git a/utils/safe-bash.sh b/utils/safe-bash.sh
new file mode 100755
index 0000000..8bdec9d
--- /dev/null
+++ b/utils/safe-bash.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+if test "$#" -gt 1 -a "$1" = "-c"; then shift; fi
+bash -euET -o pipefail -c 'trap "kill $$" ERR; '"$1"
+exit $?