author | wenzelm |
Tue, 13 Feb 2001 01:32:54 +0100 | |
changeset 11103 | 2a3cc8e1723a |
parent 11102 | 5ceaa79c220d |
child 11104 | f2024fed9f0c |
etc/settings | file | annotate | diff | comparison | revisions |
--- a/etc/settings Mon Feb 12 20:47:19 2001 +0100 +++ b/etc/settings Tue Feb 13 01:32:54 2001 +0100 @@ -129,6 +129,7 @@ #The dvi file viewer DVI_VIEWER=xdvi #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" +#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"