Bug fix: directory creation.

This commit is contained in:
Achim D. Brucker 2018-04-07 21:52:35 +01:00
parent 313a6ea930
commit 5e3bdbd340
1 changed files with 4 additions and 4 deletions

View File

@ -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