aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rwxr-xr-xtools/distclean3
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