diff options
Diffstat (limited to 'doc/waft')
| -rw-r--r-- | doc/waft | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/doc/waft b/doc/waft new file mode 100644 index 0000000000..4e526ca9a1 --- /dev/null +++ b/doc/waft @@ -0,0 +1,17 @@ +#!/bin/sh +# +# Copyright (C) Paul Davis 2011-2012 + +while true ; do + if [ -x ./waf ] ; then + ./waf "$@" + if [ "$?" -ne "0" ]; then + exit 1 + else + exit 0 + fi + fi + cd .. + if [ `pwd` = '/' ] ; then break; fi +done + |