Enable Bash pipefail so that e.g. wget failure leads to download failure

1 files changed, 3 insertions, 1 deletions

diff --git a/download b/download
index 55e06225db2d..89efbbe451fb 100755
--- a/download
+++ b/download
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 #*************************************************************************
 #
 # DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
@@ -26,6 +26,8 @@
 #
 #*************************************************************************
 
+set -o pipefail
+
 # environment setup yet?
 if [ -z "$TARFILE_LOCATION" ]; then
     . ./config_host.mk