| author | wenzelm |
| Fri, 18 Aug 2000 17:53:49 +0200 | |
| changeset 9650 | 6f0b89f2a1f9 |
| 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 |