| changeset 48985 | 5386df44a037 |
| parent 48956 | d54a3d39ba85 |
| child 53498 | 05313b45a5ae |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Main/document/build Tue Aug 28 18:57:32 2012 +0200 @@ -0,0 +1,13 @@ +#!/bin/bash + +set -e + +FORMAT="$1" +VARIANT="$2" + +"$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . + +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_TOOL" latex -o "$FORMAT" +