Bug fix: directory creation.

2018-04-07 21:44:26 +01:00 · 2018-04-07 21:44:26 +01:00 · 313a6ea930
parent e4f5f9bf68
commit 313a6ea930
1 changed files with 0 additions and 2 deletions
--- a/document-generator/Tools/DOF_mkroot
+++ b/document-generator/Tools/DOF_mkroot
@ -90,8 +90,6 @@ else
 fi


-[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
-
 if [ "$DOC" = true ]; then
  $ISABELLE_TOOL mkroot -d -n "$NAME"
  echo "    \"build\"" >> ROOT