# HG changeset patch
# User wenzelm
# Date 1343840237 -7200
# Node ID 547b075669ae700e7ddf9314d4d9b8012af8a343
# Parent  38793f924c9aa3cf270d8332650d0534ddaa692f
more precise guide for bibtex/makeindex -- dummy files should be sufficient;

diff -r 38793f924c9a -r 547b075669ae lib/Tools/document
--- a/lib/Tools/document	Wed Aug 01 15:56:36 2012 +0200
+++ b/lib/Tools/document	Wed Aug 01 18:57:17 2012 +0200
@@ -122,8 +122,8 @@
   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
   "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
-  { [ ! -f root.bib -a ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
-  { [ ! -f root.idx -a ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
+  { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
+  { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
   "$ISABELLE_TOOL" latex -o "$FMT"
 }