| changeset 73724 | 5a3a2a52648d |
| parent 62589 | b5783412bfed |
| child 73725 | cd9afbd0ccb9 |
--- a/src/Doc/prepare_document Tue May 18 15:17:55 2021 +0200 +++ b/src/Doc/prepare_document Tue May 18 15:46:03 2021 +0200 @@ -4,7 +4,6 @@ FORMAT="$1" -isabelle latex -o sty cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . isabelle latex -o "$FORMAT" @@ -13,4 +12,3 @@ isabelle latex -o "$FORMAT" [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out isabelle latex -o "$FORMAT" -