diff options
| -rw-r--r-- | isa/interface | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/isa/interface b/isa/interface index 46c78a58..9f2d33a6 100644 --- a/isa/interface +++ b/isa/interface @@ -183,7 +183,7 @@ else [ "$INITFILE" = false ] && ARGS="$ARGS -q" if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then - ARGS="$ARGS -T Isabelle" + #ARGS="$ARGS -T Isabelle" [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts else ARGS="$ARGS -nw" |