From cceb9841341d64c48f454e0ed146926736de2313 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 4 Jun 2018 10:36:26 +0100 Subject: [PATCH] Added support for selecting different document templates. --- document-generator/Tools/DOF_mkroot | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot index 0e296888..89c31ba5 100755 --- a/document-generator/Tools/DOF_mkroot +++ b/document-generator/Tools/DOF_mkroot @@ -40,6 +40,7 @@ function usage() echo " Options are:" echo " -d enable document preparation" echo " -n NAME alternative session name (default: DIR base name)" + echo " -o TEMPLATE alternative setup for root.tex (default: basic support using scrreprt)" echo echo " Prepare session root DIR (default: current directory)." echo @@ -59,8 +60,9 @@ function fail() DOC="" NAME="" +TEMPLATE="" -while getopts "n:d" OPT +while getopts "o:n:d" OPT do case "$OPT" in d) @@ -69,6 +71,9 @@ do n) NAME="$OPTARG" ;; + o) + TEMPLATE="-$OPTARG" + ;; \?) usage ;; @@ -95,7 +100,9 @@ if [ "$DOC" = true ]; then echo " \"build\"" >> "$DIR"/ROOT TITLE=$(echo "$NAME" | tr _ - | tr -d '\\') AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') - cp "$ISABELLE_HOME_USER/DOF/document-template"/* "$DIR"/document/ + cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/ + cp "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" "$DIR"/document/ + cp "$ISABELLE_HOME_USER/DOF/document-template/root$TEMPLATE.tex" "$DIR"/document/root.tex sed -i -e "s//$AUTHOR/" -e "s//$TITLE/" "$DIR"/document/root.tex else $ISABELLE_TOOL mkroot -n "$NAME"