lib/Tools/latex
changeset 11845 6d9d2b1d455d
parent 10555 2323ec838401
child 12846 0fce95478e19
     1.1 --- a/lib/Tools/latex	Sat Oct 20 20:15:27 2001 +0200
     1.2 +++ b/lib/Tools/latex	Sat Oct 20 20:15:44 2001 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     1.5  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     1.6  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
     1.7 -function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
     1.8 +function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
     1.9  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.10  
    1.11  function update_styles ()