etc/settings
changeset 2352 562cb286138e
parent 2345 8e45991e3601
child 2410 a0727e4d9453
     1.1 --- a/etc/settings	Mon Dec 09 16:48:30 1996 +0100
     1.2 +++ b/etc/settings	Mon Dec 09 16:51:14 1996 +0100
     1.3 @@ -65,4 +65,5 @@
     1.4  
     1.5  ## misc
     1.6  
     1.7 -DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
     1.8 +#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
     1.9 +DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"