diff -r 2c3d4e03e00c -r 2be239143d42 lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Fri Sep 01 19:40:57 2000 +0200
+++ b/lib/scripts/isa-xterm	Fri Sep 01 19:42:11 2000 +0200
@@ -104,7 +104,7 @@
 PASS="$PASS_MODE $PASS"
 
 if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
-  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e \"$ISABELLE\" $PASS "$@"
+  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e "$ISABELLE" $PASS "$@"
 else
   $ISATOOL installfonts
   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
@@ -121,5 +121,5 @@
     -xrm "*VT100*font5:" \
     -xrm "*fontMenu*font6*Label:" \
     -xrm "*VT100*font6:" \
-    -e \"$ISABELLE\" -m isabelle_font -m symbols $PASS "$@"
+    -e "$ISABELLE" -m isabelle_font -m symbols $PASS "$@"
 fi