equal
deleted
inserted
replaced
4 |
4 |
5 FORMAT="$1" |
5 FORMAT="$1" |
6 VARIANT="$2" |
6 VARIANT="$2" |
7 |
7 |
8 # ad-hoc patching of temporary path from sources |
8 # ad-hoc patching of temporary path from sources |
9 perl -i -pe 's/\\isakeyword\{module\{\\isacharunderscore\}name\}\\ Example\\ \\isakeyword\{file\}\\ \{\\isachardoublequoteopen\}.*\{\\isacharslash\}/\\isakeyword{module{\\isacharunderscore}name}\\ Example\\ \\isakeyword{file}\\ {\\isachardoublequoteopen}examples{\\isacharslash}/g' \ |
9 perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex |
10 Introduction.tex |
|
11 |
10 |
12 "$ISABELLE_TOOL" logo Isar |
11 "$ISABELLE_TOOL" logo Isar |
13 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" |
12 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" |
14 |
13 |
15 # clean up afterwards |
14 # clean up afterwards |