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