From b4d70883ba829fdc9934d08680bb35c669dac78e Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 4 Jun 2018 11:22:09 +0100 Subject: [PATCH] Added list of available templates to help messages. --- document-generator/Tools/DOF_mkroot | 12 +++++++++--- .../{root.tex => root-default-scrreprt.tex} | 0 2 files changed, 9 insertions(+), 3 deletions(-) rename document-generator/document-template/{root.tex => root-default-scrreprt.tex} (100%) diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot index 89c31ba5..a5acc7cf 100755 --- a/document-generator/Tools/DOF_mkroot +++ b/document-generator/Tools/DOF_mkroot @@ -41,6 +41,12 @@ function usage() 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 " Available templates:" + for t in "$ISABELLE_HOME_USER/DOF/document-template/"*.tex; do + if [[ $t =~ root-(.*).tex$ ]]; then + echo " * ${BASH_REMATCH[1]}" + fi + done echo echo " Prepare session root DIR (default: current directory)." echo @@ -60,7 +66,7 @@ function fail() DOC="" NAME="" -TEMPLATE="" +TEMPLATE="default-scrreprt" while getopts "o:n:d" OPT do @@ -72,7 +78,7 @@ do NAME="$OPTARG" ;; o) - TEMPLATE="-$OPTARG" + TEMPLATE="$OPTARG" ;; \?) usage @@ -102,7 +108,7 @@ if [ "$DOC" = true ]; then AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') 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 + 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" diff --git a/document-generator/document-template/root.tex b/document-generator/document-template/root-default-scrreprt.tex similarity index 100% rename from document-generator/document-template/root.tex rename to document-generator/document-template/root-default-scrreprt.tex