author | wenzelm |
Thu, 11 Feb 1999 21:19:56 +0100 | |
changeset 6277 | 6e64b1cc76f8 |
parent 6276 | ae60af165213 |
child 6278 | 37b76155a49e |
--- a/lib/scripts/isa-xterm Thu Feb 11 21:18:56 1999 +0100 +++ b/lib/scripts/isa-xterm Thu Feb 11 21:19:56 1999 +0100 @@ -101,5 +101,5 @@ -xrm "*VT100*font5:" \ -xrm "*fontMenu*font6*Label:" \ -xrm "*VT100*font6:" \ - -e $ISABELLE -m symbols $PASS "$@" + -e $ISABELLE -m isabelle_font -m symbols $PASS "$@" fi