Commit f71f3427 authored by Sebastian Graf's avatar Sebastian Graf

Make `git clean -nxd` silent after `make distclean`

Also check that invariant in CI: After a `make distclean`
`git clean -nxd` should find no files.

The hope is that this catches cases were a `make clean` would forget to
list a `.gitignore`d file that should either be registered as a
`(DIST_)CLEAN_FILES` or should be unignored and committed into the
parent 8632268a
......@@ -11,3 +11,13 @@ validate:
- make boot mode=fast
- "make mode=fast NoFibRuns=1 2>&1 | tee log"
- "nofib-analyse/nofib-analyse log"
- |
# The following checks that `make distclean` removes any files reported
# by `git clean -fxd`
make distclean
files=$(git clean -nxd | cut -d" " -f3 | sed "/log/d")
if ! [ -z $files ]
echo "The following files weren't cleaned:\n$files"
exit 1
......@@ -10,8 +10,17 @@ all :: $(PROG)
boot :: $(PROG)
rm -f $(PROG)
# This clean hierarchy mirrors mk/
# See mk/ for the semantics.
.PHONY: mostlyclean clean distclean maintainer-clean
rm -f CmdLine.hi GenUtils.hi Main.hi Slurp.hi
rm -f CmdLine.o GenUtils.o Main.o Slurp.o
clean:: mostlyclean
rm -f $(PROG)
distclean:: clean
maintainer-clean:: distclean
......@@ -5,3 +5,5 @@ include $(TOP)/mk/
FAST_OPTS = runtime_files/fast
NORM_OPTS = runtime_files/norm
SLOW_OPTS = runtime_files/slow
CLEAN_FILES += runtime_files/*.tex
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment