| changeset 73731 | a1ef2589c33f |
| parent 73723 | 1bbbaae6b5e3 |
| child 73733 | b13b2c1d419e |
--- a/src/Doc/Tutorial/document/build Tue May 18 17:19:19 2021 +0200 +++ b/src/Doc/Tutorial/document/build Tue May 18 19:49:06 2021 +0200 @@ -9,5 +9,4 @@ isabelle latex -o bbl ./isa-index root isabelle latex -o "$FORMAT" -[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out isabelle latex -o "$FORMAT"