# HG changeset patch # User wenzelm # Date 852624293 -3600 # Node ID dae7f8ca50013c4d26ba37d57d2d3e1d00bfb17a # Parent 36bdba95e170c55c6a5c721fb51ba47f26e36dd0 added dvi viewer alternative; diff -r 36bdba95e170 -r dae7f8ca5001 etc/settings --- a/etc/settings Tue Jan 07 09:03:53 1997 +0100 +++ b/etc/settings Tue Jan 07 09:04:53 1997 +0100 @@ -63,6 +63,7 @@ ISABELLE_DOCS=$ISABELLE_HOME/doc #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" +#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"