diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 12:40:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 12:40:09 +0000 |
| commit | 9de1c3b41bb4dd85e4a501c53666a7fd72228621 (patch) | |
| tree | e8a06fd58a75479d3c024eb837954cf15d72cefc | |
| parent | 65040f942717d5b8b5aaf3bf14bbfa76a128c832 (diff) | |
Prevent setting WM title so Emacs can do its own thing
| -rw-r--r-- | isar/interface | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/interface b/isar/interface index 46c78a58..9f2d33a6 100644 --- a/isar/interface +++ b/isar/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" |