etc/settings
changeset 53883 eec610972763
parent 53880 a7d69a11f395
child 53927 6150cf05f729
     1.1 --- a/etc/settings	Sat Jul 27 22:16:04 2013 +0200
     1.2 +++ b/etc/settings	Sat Jul 27 22:20:25 2013 +0200
     1.3 @@ -39,7 +39,6 @@
     1.4  ISABELLE_PDFLATEX="pdflatex"
     1.5  ISABELLE_BIBTEX="bibtex"
     1.6  ISABELLE_MAKEINDEX="makeindex"
     1.7 -ISABELLE_DVIPS="dvips -D 600"
     1.8  ISABELLE_EPSTOPDF="epstopdf"
     1.9  
    1.10  # Paranoia setting for strange latex installations ...