# HG changeset patch
# User wenzelm
# Date 1003601744 -7200
# Node ID 6d9d2b1d455dfd01efe516a74114154d9c174e6e
# Parent  eb072fd9a45ab53eca6fa9f7c3c4b149608c062f
dvips -q;

diff -r eb072fd9a45a -r 6d9d2b1d455d lib/Tools/latex
--- a/lib/Tools/latex	Sat Oct 20 20:15:27 2001 +0200
+++ b/lib/Tools/latex	Sat Oct 20 20:15:44 2001 +0200
@@ -76,7 +76,7 @@
 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
-function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
+function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 
 function update_styles ()