lib/Tools/document
changeset 8269 d28f549105fe
parent 8217 dc3b8cdbb816
child 8654 38ce936acb99
--- a/lib/Tools/document	Mon Feb 21 13:57:07 2000 +0100
+++ b/lib/Tools/document	Mon Feb 21 14:08:15 2000 +0100
@@ -81,7 +81,7 @@
 function pre_latex ()
 {
   local FMT="$1"
-  rm -f *.aux
+  rm -f *.aux *.out
   if [ -f root.bib ]
   then
     $ISATOOL latex -o "$FMT" && \