equal
deleted
inserted
replaced
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/* |