diff -r d243553849ec -r efb3428c9879 bin/isabelle
--- a/bin/isabelle	Wed Nov 22 21:38:26 2000 +0100
+++ b/bin/isabelle	Wed Nov 22 21:41:39 2000 +0100
@@ -9,9 +9,9 @@
 
 ## settings
 
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
 
-ISABELLE_HOME=$(dirname "$0")/..
+ISABELLE_HOME="$(dirname "$0")/.."
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }