| changeset 73748 | e78c8a1f03fb |
| parent 73747 | 8c460c09665e |
| child 73749 | 6ddbb74a52c9 |
--- a/src/Doc/Codegen/document/build Wed May 19 16:35:10 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -# ad-hoc patching of temporary path from sources -perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex - -"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - -# clean up afterwards -rm -rf "${ISABELLE_TMP}/examples"