From: Ben Pfaff 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