0.6.12.7.flaky1.1:

[sbcl.git] / clean.sh

diff --git a/clean.sh b/clean.sh
index 72ad69d..57a9c50 100755 (executable)
--- a/clean.sh
+++ b/clean.sh
@@ -26,7 +26,12 @@ rm -rf obj/* output/* doc/user-manual \
 pwd=`pwd`
 for d in tools-for-build; do
     cd $d
-    make clean
+    # I hope the -s option is standard. At least GNU make and BSD make
+    # support it. It silences make, since otherwise the output from
+    # this script is just the operations done by these make's, which
+    # is misleading when this script does lotso other operations too.
+    # -- WHN
+    make -s clean
     cd $pwd
 done