# HG changeset patch
# User wenzelm
# Date 850146674 -3600
# Node ID 562cb286138e7a8443f5c3977d2913a8f8253bcd
# Parent  873ffd6f70c352a56af1ce8088b79b8a4e889922
added DVI_VIEWER for 600dpi fonts;

diff -r 873ffd6f70c3 -r 562cb286138e etc/settings
--- 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"