diff -r 348ec44248df -r 4167688e58aa 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