equal
deleted
inserted
replaced
175 */*) |
175 */*) |
176 OUTFILE="$OUTPUT" |
176 OUTFILE="$OUTPUT" |
177 ;; |
177 ;; |
178 *) |
178 *) |
179 mkdir -p "$ISABELLE_OUTPUT" |
179 mkdir -p "$ISABELLE_OUTPUT" |
|
180 chmod $(umask -S) "$ISABELLE_OUTPUT" |
180 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
181 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
181 ;; |
182 ;; |
182 esac |
183 esac |
183 |
184 |
184 |
185 |
186 |
187 |
187 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
188 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
188 ISABELLE_PID="$$" |
189 ISABELLE_PID="$$" |
189 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
190 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
190 mkdir -p "$ISABELLE_TMP" |
191 mkdir -p "$ISABELLE_TMP" |
|
192 chmod $(umask -S) "$ISABELLE_TMP" |
191 |
193 |
192 |
194 |
193 ## run it! |
195 ## run it! |
194 |
196 |
195 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
197 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |