added dvi viewer alternative;
authorwenzelm
Tue Jan 07 09:04:53 1997 +0100 (1997-01-07)
changeset 2476dae7f8ca5001
parent 2475 36bdba95e170
child 2477 ff44d0e1953a
added dvi viewer alternative;
etc/settings
     1.1 --- a/etc/settings	Tue Jan 07 09:03:53 1997 +0100
     1.2 +++ b/etc/settings	Tue Jan 07 09:04:53 1997 +0100
     1.3 @@ -63,6 +63,7 @@
     1.4  ISABELLE_DOCS=$ISABELLE_HOME/doc
     1.5  
     1.6  #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
     1.7 +#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
     1.8  DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
     1.9  
    1.10