diff -r dfe444b748aa -r 05b6e5bcab66 lib/Tools/mkdir
--- 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