tuned comments;
authorwenzelm
Mon Feb 17 12:00:00 1997 +0100 (1997-02-17)
changeset 2643a7f469c0ba59
parent 2642 3c3a84cc85a9
child 2644 2fa0f0c1c750
tuned comments;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Mon Feb 17 11:04:00 1997 +0100
     1.2 +++ b/lib/scripts/getsettings	Mon Feb 17 12:00:00 1997 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  set -o allexport
     1.6  
     1.7 -#users tend to put strange things in here
     1.8 +#users tend to put strange things in here ...
     1.9  unset ENV
    1.10  unset BASH_ENV
    1.11  
    1.12 @@ -18,6 +18,7 @@
    1.13  unset OSTYPE
    1.14  PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
    1.15  
    1.16 +#get actual settings
    1.17  . $ISABELLE_HOME/etc/settings || exit 2
    1.18  [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    1.19