2011-11-07 13:46:58 -06:00
|
|
|
#!/bin/sh
|
|
|
|
|
|
|
|
|
|
EHOME=`echo $HOME | sed "s/#/\#/"`
|
2011-11-07 16:52:18 -06:00
|
|
|
DIR=$PLUMA_CURRENT_DOCUMENT_DIR
|
2011-11-07 13:46:58 -06:00
|
|
|
while test "$DIR" != "/"; do
|
|
|
|
|
for m in GNUmakefile makefile Makefile; do
|
|
|
|
|
if [ -f "${DIR}/${m}" ]; then
|
|
|
|
|
echo "Using ${m} from ${DIR}" | sed "s#$EHOME#~#" > /dev/stderr
|
|
|
|
|
make -C "${DIR}"
|
|
|
|
|
exit
|
|
|
|
|
fi
|
|
|
|
|
done
|
|
|
|
|
DIR=`dirname "${DIR}"`
|
|
|
|
|
done
|
|
|
|
|
echo "No Makefile found!" > /dev/stderr
|
