| changeset 73731 | a1ef2589c33f |
| parent 73725 | cd9afbd0ccb9 |
| child 73733 | b13b2c1d419e |
--- a/src/Doc/prepare_document Tue May 18 17:19:19 2021 +0200 +++ b/src/Doc/prepare_document Tue May 18 19:49:06 2021 +0200 @@ -8,5 +8,4 @@ isabelle latex -o bbl [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root isabelle latex -o "$FORMAT" -[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out isabelle latex -o "$FORMAT"