fi
fi
e() { echo "$0: $*"; "$@"; }
- errcatch-cleanup() { stop; }
+ err-cleanup() { stop; }
modify
# we leave it as is even when stopping, because we would like it to be default, but the only way
# to change the default is for every device, and I want to avoid that, even though I wouldn't mind, others users of this script might.