# HG changeset patch # User wenzelm # Date 1360239605 -3600 # Node ID 70a4c11cd79eecec7cf08bdee862b75935527975 # Parent bece235e305408ba2435058f8dea50e7a7f49398 proper root for document variants (cf. be8002ee43d8); diff -r bece235e3054 -r 70a4c11cd79e lib/Tools/document --- a/lib/Tools/document Thu Feb 07 12:08:37 2013 +0100 +++ b/lib/Tools/document Thu Feb 07 13:20:05 2013 +0100 @@ -124,7 +124,7 @@ "$ISABELLE_TOOL" latex -o "$FMT" "$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" + "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" } (