| changeset 64375 | 74a2af7c5145 |
| parent 64370 | 865b39487b5d |
| child 64483 | bba1d341bdf6 |
| 64374:80d498d56116 | 64375:74a2af7c5145 |
|---|---|
240 do |
240 do |
241 echo " $FILE" |
241 echo " $FILE" |
242 done |
242 done |
243 } |
243 } |
244 |
244 |
245 rm -f "$TARGET" |
|
245 rm -rf classes && mkdir classes |
246 rm -rf classes && mkdir classes |
246 |
247 |
247 SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes" |
248 SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes" |
248 |
249 |
249 ( |
250 ( |