From: Ben Pfaff <blp@nicira.com>
Date: Tue, 4 Nov 2008 22:26:38 +0000 (-0800)
Subject: Use "set -e" command instead of "#! /bin/sh -e" magic.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=70ebdff4f817f0c442f3218c5d9a4e3a496e100d;p=openvswitch

Use "set -e" command instead of "#! /bin/sh -e" magic.

Otherwise, running the script through an explicit shell invocation, such
as "sh -x <script>" for debugging, will fail to set -e and therefore the
script's behavior will change.
---

diff --git a/boot.sh b/boot.sh
index 0f48d439..ae2b3665 100755
--- a/boot.sh
+++ b/boot.sh
@@ -1,4 +1,6 @@
-#! /bin/sh -e
+#! /bin/sh
+
+set -e
 
 have_ext=$(if test -e ext/automake.mk; then echo yes; else echo no; fi)
 for opt
diff --git a/secchan/commands/update b/secchan/commands/update
index 4d617fea..545e3c23 100755
--- a/secchan/commands/update
+++ b/secchan/commands/update
@@ -1,3 +1,4 @@
-#! /bin/sh -e
+#! /bin/sh
+set -e
 apt-get update -qy
 apt-get upgrade -qy
diff --git a/utilities/ofp-pki.in b/utilities/ofp-pki.in
index 89a3dba0..7d51469b 100755
--- a/utilities/ofp-pki.in
+++ b/utilities/ofp-pki.in
@@ -1,4 +1,6 @@
-#! /bin/sh -e
+#! /bin/sh
+
+set -e
 
 pkidir='@PKIDIR@'
 command=