more precise guide for bibtex/makeindex -- dummy files should be sufficient;
authorwenzelm
Wed, 01 Aug 2012 18:57:17 +0200
changeset 48637 547b075669ae
parent 48636 38793f924c9a
child 48638 22d65e375c01
more precise guide for bibtex/makeindex -- dummy files should be sufficient;
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"
 }