diff -r e7418f8d49fe -r d468d72a458f doc-src/System/document/build
--- a/doc-src/System/document/build	Mon Aug 27 16:48:41 2012 +0200
+++ b/doc-src/System/document/build	Mon Aug 27 17:11:55 2012 +0200
@@ -22,4 +22,6 @@
 "$ISABELLE_TOOL" latex -o "$FORMAT"
 "$ISABELLE_TOOL" latex -o "$FORMAT"
 "$ISABELLE_HOME/doc-src/sedindex" root
+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
 "$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"