# HG changeset patch
# User wenzelm
# Date 857145272 -3600
# Node ID 4167688e58aa1456714a96ea60d3fa1a38380d63
# Parent  348ec44248dfb395e437859c2ac33d97d854be53
now uses -m symbols;

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