--- a/bin/isabelle Wed Mar 05 17:15:31 1997 +0100
+++ b/bin/isabelle Thu Mar 06 12:28:17 1997 +0100
@@ -9,21 +9,9 @@
PRG=$(basename $0)
-ISABELLE_HOME=$(dirname $(dirname $0))
-case "$ISABELLE_HOME" in
- /*)
- if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
- . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
- else
- echo "ERROR: $PRG probably not called from its original place!"
- exit 1
- fi
- ;;
- *)
- echo "ERROR: $PRG not called with absolute path specification!"
- exit 1
- ;;
-esac
+ISABELLE_HOME=$(dirname $0)/..
+. $ISABELLE_HOME/lib/scripts/getsettings || \
+ { echo "$PRG probably not called from its original place!"; exit 2 }
## diagnostics