From 5e3bdbd340c809bc3cc87eb555a0736a1856c4cf Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sat, 7 Apr 2018 21:52:35 +0100
Subject: [PATCH] Bug fix: directory creation.

---
 document-generator/Tools/DOF_mkroot | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot
index d56b3acf..0e296888 100755
--- a/document-generator/Tools/DOF_mkroot
+++ b/document-generator/Tools/DOF_mkroot
@@ -91,12 +91,12 @@ fi
 
 
 if [ "$DOC" = true ]; then
-  $ISABELLE_TOOL mkroot -d -n "$NAME"
-  echo "    \"build\"" >> ROOT
+  $ISABELLE_TOOL mkroot -d -n "$NAME" "$DIR"
+  echo "    \"build\"" >> "$DIR"/ROOT
   TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
-  cp "$ISABELLE_HOME_USER/DOF/document-template"/* document/
-  sed -i -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" document/root.tex
+  cp "$ISABELLE_HOME_USER/DOF/document-template"/* "$DIR"/document/
+  sed -i -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" "$DIR"/document/root.tex
 else
     $ISABELLE_TOOL mkroot -n "$NAME"
 fi