-#!/bin/bash -x
+#!/bin/bash
# Set grub to boot into a different distro, and reboot unless -r
# $0 [DISTRO_NAME]
# DISTRO_NAME is based on the partition names in /boot. eg boot_debianjessie
set -eE -o pipefail
-trap 'echo "$0:$LINENO:error: \"$BASH_COMMAND\" returned $?"' ERR
+trap 'echo "$0:$LINENO:error: \"$BASH_COMMAND\" returned $?" >&2' ERR
[[ $EUID == 0 ]] || exec sudo "$BASH_SOURCE" "$@"
reboot=true
while [[ $1 == -* ]]; do
case $1 in
+ -d) set -x; shift ;;
-r) reboot=false; shift ;;
--) break ;;
esac
e umount $mount_point
e rmdir $mount_point
+
+if $reboot; then
+ reboot now
+fi