--- a/lib/scripts/getsettings Mon Jun 06 08:18:43 2005 +0200
+++ b/lib/scripts/getsettings Mon Jun 06 09:28:28 2005 +0200
@@ -48,7 +48,7 @@
[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
{ echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
- source "$ISABELLE_HOME_USER/etc/settings" || exit 2
+ { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
#append ML system identifier to paths
if [ -z "$ML_PLATFORM" ]; then