diff options
| -rwxr-xr-x | etc/guix-install.sh | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/etc/guix-install.sh b/etc/guix-install.sh index 8eb5214049..dc8de2fe92 100755 --- a/etc/guix-install.sh +++ b/etc/guix-install.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/bin/sh # GNU Guix --- Functional package management for GNU # Copyright © 2017 sharlatan <sharlatanus@gmail.com> # Copyright © 2018 Ricardo Wurmus <rekado@elephly.net> @@ -19,6 +19,13 @@ # You should have received a copy of the GNU General Public License # along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. +# We require Bash but for portability we'd rather not use /bin/bash or +# /usr/bin/env in the shebang, hence this hack. +if [ "x$BASH_VERSION" = "x" ] +then + exec bash "$0" "$@" +fi + set -e [ "$UID" -eq 0 ] || { echo "This script must be run as root."; exit 1; } |