etc/settings
changeset 2352 562cb286138e
parent 2345 8e45991e3601
child 2410 a0727e4d9453
equal deleted inserted replaced
2351:873ffd6f70c3 2352:562cb286138e
    63 #ML_SYSTEM=smlnj-1.09
    63 #ML_SYSTEM=smlnj-1.09
    64 
    64 
    65 
    65 
    66 ## misc
    66 ## misc
    67 
    67 
    68 DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
    68 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
       
    69 DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"