changed xterm geometry;
authorwenzelm
Fri Dec 20 16:10:30 1996 +0100 (1996-12-20)
changeset 24665220fb014f8a
parent 2465 44ee3255555c
child 2467 357adb429fda
changed xterm geometry;
etc/settings
etc/user-settings.sample
     1.1 --- a/etc/settings	Fri Dec 20 10:54:01 1996 +0100
     1.2 +++ b/etc/settings	Fri Dec 20 16:10:30 1996 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4  
     1.5  # Xterm with symbol font.
     1.6  ISABELLE_INTERFACE=xterm
     1.7 -ISABELLE_INTERFACE_OPTIONS="-geometry 80x52"
     1.8 +ISABELLE_INTERFACE_OPTIONS="-geometry 80x60"
     1.9  ISABELLE_SYMBOLS=true
    1.10  
    1.11  # GNU Emacs running Isamode.
     2.1 --- a/etc/user-settings.sample	Fri Dec 20 10:54:01 1996 +0100
     2.2 +++ b/etc/user-settings.sample	Fri Dec 20 16:10:30 1996 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  # Xterm with symbol font.
     2.6  #ISABELLE_INTERFACE=xterm
     2.7 -#ISABELLE_INTERFACE_OPTIONS="-geometry 80x52"
     2.8 +#ISABELLE_INTERFACE_OPTIONS="-geometry 80x60"
     2.9  #ISABELLE_SYMBOLS=true
    2.10  
    2.11  # GNU Emacs running Isamode.