From 14d85dcfe91fa36a485a591c11009ffeb24259d5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 15 Apr 2004 17:07:59 +0000
Subject: Remove title setting

---
 isa/interface | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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"
-- 
cgit v1.2.3