author | webertj |
Fri, 26 Mar 2004 12:21:50 +0100 | |
changeset 14487 | 157d0ea7b2da |
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 |