diff options
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/distclean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/distclean b/tools/distclean index 6035a6d..f5e0ece 100755 --- a/tools/distclean +++ b/tools/distclean | |||
@@ -12,10 +12,9 @@ fi | |||
12 | 12 | ||
13 | if [ -f Makefile ]; then | 13 | if [ -f Makefile ]; then |
14 | echo "$0: Makefile present. Cleaning up with 'make distclean'..." | 14 | echo "$0: Makefile present. Cleaning up with 'make distclean'..." |
15 | make distclean | 15 | make -i distclean |
16 | if [ $? -ne 0 ]; then | 16 | if [ $? -ne 0 ]; then |
17 | echo "Uh-oh! Make distclean failed." | 17 | echo "Uh-oh! Make distclean failed." |
18 | echo "Please run './config.status' and try again." | ||
19 | exit 1 | 18 | exit 1 |
20 | fi | 19 | fi |
21 | fi | 20 | fi |