| author | huffman |
| Thu, 26 May 2005 02:23:27 +0200 | |
| changeset 16081 | 81a4b4a245b0 |
| parent 9522 | bf459ea9a523 |
| permissions | -rwxr-xr-x |
|
9522
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
1 |
#/!bin/bash |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
2 |
|
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
3 |
ISATOOL=${ISATOOL:-isatool}
|
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
4 |
type -p "$ISATOOL" >/dev/null || { echo "isatool not found!" >&2; exit 2; }
|
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
5 |
|
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
6 |
for FILE in $(find . -name IsaMakefile -print) |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
7 |
do |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
8 |
DIR=$(dirname "$FILE") |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
9 |
echo "Entering $DIR ..." |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
10 |
( cd "$DIR"; $ISATOOL make "$@"; ) |
|
bf459ea9a523
invoke isatool make in any dir containing an IsaMakefile;
wenzelm
parents:
diff
changeset
|
11 |
done |