handle dir prefix;
authorwenzelm
Mon Apr 10 23:38:02 2000 +0200 (2000-04-10)
changeset 868505b6e5bcab66
parent 8684 dfe444b748aa
child 8686 5893f2952e4f
handle dir prefix;
lib/Tools/mkdir
     1.1 --- a/lib/Tools/mkdir	Mon Apr 10 23:36:19 2000 +0200
     1.2 +++ b/lib/Tools/mkdir	Mon Apr 10 23:38:02 2000 +0200
     1.3 @@ -71,22 +71,26 @@
     1.4  
     1.5  if [ $# -eq 1 ]; then
     1.6    LOGIC="$ISABELLE_LOGIC"
     1.7 -  NAME="$1"; shift
     1.8 +  DIR_NAME="$1"; shift
     1.9  elif [ $# -eq 2 ]; then
    1.10    LOGIC="$1"; shift
    1.11 -  NAME="$1"; shift
    1.12 +  DIR_NAME="$1"; shift
    1.13  else
    1.14    usage
    1.15  fi
    1.16  
    1.17 -[ -z "$SESSION" ] && SESSION=$(basename $NAME)
    1.18 -
    1.19 +DIR=$(dirname "$DIR_NAME")
    1.20 +NAME=$(basename "$DIR_NAME")
    1.21  
    1.22  
    1.23  ## main
    1.24  
    1.25  # IsaMakefile
    1.26  
    1.27 +mkdir -p "$DIR" || fail "Bad directory: $DIR"
    1.28 +cd "$DIR"
    1.29 +
    1.30 +
    1.31  DOCUMENT_ROOT=""
    1.32  
    1.33  if [ -n "$BUILD" ]; then