lib/scripts/isa-xterm
changeset 2702 4167688e58aa
parent 2623 6a7372c9ca0f
child 2712 44a657985de1
--- 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