| changeset 48938 | d468d72a458f |
| parent 48937 | e7418f8d49fe |
| child 48956 | d54a3d39ba85 |
--- 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"