1.1 --- a/lib/scripts/getsettings	Fri Sep 01 17:50:36 2000 +0200
     1.2 +++ b/lib/scripts/getsettings	Fri Sep 01 17:54:58 2000 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  #
     1.5  # $Id$
     1.6 +# Author: Markus Wenzel, TU Muenchen
     1.7 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  #
     1.9  # getsettings - bash source script to augment current env.
    1.10  #
    1.11 @@ -12,11 +14,11 @@
    1.12  ISABELLE_SETTINGS_PRESENT=true
    1.13  
    1.14  #normalize ISABELLE_HOME as passed by caller
    1.15 -ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
    1.16 +ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD")
    1.17  
    1.18  #main executables
    1.19 -ISABELLE=$ISABELLE_HOME/bin/isabelle
    1.20 -ISATOOL=$ISABELLE_HOME/bin/isatool
    1.21 +ISABELLE="$ISABELLE_HOME/bin/isabelle"
    1.22 +ISATOOL="$ISABELLE_HOME/bin/isatool"
    1.23  
    1.24  #users tend to put strange things in here ...
    1.25  unset ENV
    1.26 @@ -38,9 +40,12 @@
    1.27  }
    1.28  
    1.29  #get actual settings
    1.30 -. $ISABELLE_HOME/etc/settings || exit 2
    1.31 +. "$ISABELLE_HOME/etc/settings" || exit 2
    1.32  ISABELLE_SITE_SETTINGS_PRESENT=true
    1.33 -[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    1.34 +
    1.35 +[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
    1.36 +  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
    1.37 +[ -f "$ISABELLE_HOME_USER/etc/settings" ] && . "$ISABELLE_HOME_USER/etc/settings"
    1.38  
    1.39  #append ML system identifier to paths
    1.40  if [ -z "$ML_PLATFORM" ]; then
    1.41 @@ -49,8 +54,6 @@
    1.42    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
    1.43  fi
    1.44  ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
    1.45 -ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done)
    1.46 -ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
    1.47  
    1.48  set +o allexport
    1.49