diff -r a8a21d7a83a1 -r 4412debd3004 etc/settings --- a/etc/settings Sat Oct 09 16:18:16 1999 +0200 +++ b/etc/settings Sat Oct 09 23:15:40 1999 +0200 @@ -58,6 +58,7 @@ TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" ISABELLE_LATEX="latex" ISABELLE_PDFLATEX="pdflatex" +ISABELLE_BIBTEX="bibtex" ISABELLE_DVIPS="dvips -D 600"