lib/Tools/install
changeset 5367 33f81e980c93
parent 5362 29ce4f1fe72c
child 5398 81936a99a3b0
equal deleted inserted replaced
5366:8521cd8b0a40 5367:33f81e980c93
    33 [ $# -ne 0 -o -z "$DIR" -o "$DIR" = "-?" ] && usage
    33 [ $# -ne 0 -o -z "$DIR" -o "$DIR" = "-?" ] && usage
    34 
    34 
    35 
    35 
    36 ## main
    36 ## main
    37 
    37 
    38 [ ! -d "$DIR" ] && fail "Bad directory: $DIR"
    38 mkdir -p "$DIR" || fail "Bad directory: $DIR"
    39 
    39 
    40 BASH=$(type -path bash)
    40 BASH=$(type -path bash)
    41 [ -z "$BASH" ] && fail "Cannot find bash!"
    41 [ -z "$BASH" ] && fail "Cannot find bash!"
    42 
    42 
    43 for BIN in $ISABELLE_HOME/bin/*
    43 for BIN in $ISABELLE_HOME/bin/*