| changeset 3118 | 24dae6222579 |
| parent 3054 | c16029f41ad9 |
| child 3183 | 537f7281d42c |
| 3117:74c1b51c1cd9 | 3118:24dae6222579 |
|---|---|
146 ;; |
146 ;; |
147 */*) |
147 */*) |
148 OUTFILE="$OUTPUT" |
148 OUTFILE="$OUTPUT" |
149 ;; |
149 ;; |
150 *) |
150 *) |
151 mkdir -p "$ISABELLE_OUTPUT_DIR" |
151 mkdir -p "$ISABELLE_OUTPUT" |
152 OUTFILE="$ISABELLE_OUTPUT_DIR/$OUTPUT" |
152 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
153 ;; |
153 ;; |
154 esac |
154 esac |
155 |
155 |
156 |
156 |
157 ## run it! |
157 ## run it! |