# 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
# 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