|
#!/usr/bin/env bash
set -e
FORMAT="$1"
isabelle latex -o sty
cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
isabelle latex -o "$FORMAT"
isabelle latex -o bbl
[ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
isabelle latex -o "$FORMAT"
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
isabelle latex -o "$FORMAT"
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
