diff options
| author | David Aspinall | 2004-04-15 17:07:59 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-04-15 17:07:59 +0000 |
| commit | 14d85dcfe91fa36a485a591c11009ffeb24259d5 (patch) | |
| tree | 02cedf7368ad7043be790b3db979674a2550748d /isa | |
| parent | 6cd6aa64eafba38e95115fb1e8947c538ac83939 (diff) | |
Remove title setting
Diffstat (limited to 'isa')
| -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" |