# HG changeset patch # User wenzelm # Date 903971809 -7200 # Node ID 33f81e980c938bb42409b816153d77e74ef21f2d # Parent 8521cd8b0a407b64ae4c21ba231246d355ffaac1 mkdir -p; diff -r 8521cd8b0a40 -r 33f81e980c93 lib/Tools/install --- a/lib/Tools/install Mon Aug 24 17:13:58 1998 +0200 +++ b/lib/Tools/install Mon Aug 24 17:16:49 1998 +0200 @@ -35,7 +35,7 @@ ## main -[ ! -d "$DIR" ] && fail "Bad directory: $DIR" +mkdir -p "$DIR" || fail "Bad directory: $DIR" BASH=$(type -path bash) [ -z "$BASH" ] && fail "Cannot find bash!"