From a36c1566d4a74138e07ecbc45a90706ef2bc5afb Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 6 Apr 2019 13:19:27 +0100 Subject: [PATCH] Fixed printing of default template. --- document-generator/Tools/DOF_mkroot | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot index 00f7d25..fbdb026 100755 --- a/document-generator/Tools/DOF_mkroot +++ b/document-generator/Tools/DOF_mkroot @@ -48,7 +48,7 @@ function usage() echo " * ${BASH_REMATCH[1]}" fi done - echo " -t TEMPLATE (default: DEFAULT_TEMPLATE)" + echo " -t TEMPLATE (default: $DEFAULT_TEMPLATE)" echo " Available document templates:" for t in "$ISABELLE_HOME_USER/DOF/document-template/"*.tex; do if [[ $t =~ root-(.*).tex$ ]]; then