equal
deleted
inserted
replaced
69 # args |
69 # args |
70 |
70 |
71 |
71 |
72 if [ $# -eq 1 ]; then |
72 if [ $# -eq 1 ]; then |
73 LOGIC="$ISABELLE_LOGIC" |
73 LOGIC="$ISABELLE_LOGIC" |
74 NAME="$1"; shift |
74 DIR_NAME="$1"; shift |
75 elif [ $# -eq 2 ]; then |
75 elif [ $# -eq 2 ]; then |
76 LOGIC="$1"; shift |
76 LOGIC="$1"; shift |
77 NAME="$1"; shift |
77 DIR_NAME="$1"; shift |
78 else |
78 else |
79 usage |
79 usage |
80 fi |
80 fi |
81 |
81 |
82 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
82 DIR=$(dirname "$DIR_NAME") |
83 |
83 NAME=$(basename "$DIR_NAME") |
84 |
84 |
85 |
85 |
86 ## main |
86 ## main |
87 |
87 |
88 # IsaMakefile |
88 # IsaMakefile |
|
89 |
|
90 mkdir -p "$DIR" || fail "Bad directory: $DIR" |
|
91 cd "$DIR" |
|
92 |
89 |
93 |
90 DOCUMENT_ROOT="" |
94 DOCUMENT_ROOT="" |
91 |
95 |
92 if [ -n "$BUILD" ]; then |
96 if [ -n "$BUILD" ]; then |
93 IMAGES="$NAME" |
97 IMAGES="$NAME" |