now uses -m symbols;
authorwenzelm
Fri, 28 Feb 1997 16:54:32 +0100
changeset 2702 4167688e58aa
parent 2701 348ec44248df
child 2703 5ce1310560ff
now uses -m symbols;
lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Fri Feb 28 16:47:56 1997 +0100
+++ b/lib/scripts/isa-xterm	Fri Feb 28 16:54:32 1997 +0100
@@ -109,6 +109,6 @@
       -xrm "*VT100*font5:" \
       -xrm "*fontMenu*font6*Label:" \
       -xrm "*VT100*font6:" \
-      -e $ISABELLE -e 'print_mode:=["symbols"];' "$@"
+      -e $ISABELLE -m symbols "$@"
   fi
 fi