diff options
| -rwxr-xr-x | tools/distclean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/distclean b/tools/distclean index 6035a6d6..f5e0ecef 100755 --- a/tools/distclean +++ b/tools/distclean @@ -12,10 +12,9 @@ fi if [ -f Makefile ]; then echo "$0: Makefile present. Cleaning up with 'make distclean'..." - make distclean + make -i distclean if [ $? -ne 0 ]; then echo "Uh-oh! Make distclean failed." - echo "Please run './config.status' and try again." exit 1 fi fi |