# HG changeset patch
# User kleing
# Date 1118042908 -7200
# Node ID a920fe734a49a93c98206581cb8f5902482d5523
# Parent  fbe2fc30a177e447750658facec40fd1b6501c1d
fixed
(exited abnormally when ~/isabelle/etc/settings not present)

diff -r fbe2fc30a177 -r a920fe734a49 lib/scripts/getsettings
--- 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