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 6035a6d6..f5e0ecef 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 |
