--- a/lib/Tools/mkdir Mon Apr 10 23:36:19 2000 +0200
+++ b/lib/Tools/mkdir Mon Apr 10 23:38:02 2000 +0200
@@ -71,22 +71,26 @@
if [ $# -eq 1 ]; then
LOGIC="$ISABELLE_LOGIC"
- NAME="$1"; shift
+ DIR_NAME="$1"; shift
elif [ $# -eq 2 ]; then
LOGIC="$1"; shift
- NAME="$1"; shift
+ DIR_NAME="$1"; shift
else
usage
fi
-[ -z "$SESSION" ] && SESSION=$(basename $NAME)
-
+DIR=$(dirname "$DIR_NAME")
+NAME=$(basename "$DIR_NAME")
## main
# IsaMakefile
+mkdir -p "$DIR" || fail "Bad directory: $DIR"
+cd "$DIR"
+
+
DOCUMENT_ROOT=""
if [ -n "$BUILD" ]; then