--- 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