Diffusion nofib 58f710d16296

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

Authored by sgraf on Jan 8 2019, 6:45 AM.

Description

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 .gitignored file that should either be registered as a
(DIST_)CLEAN_FILE or should be unignored and committed into the
repository.

Details

Committed
sgrafJan 8 2019, 6:45 AM
Parents
rNOFIBe2d614e40e8b: Disable timer-based context switches
Branches
Unknown
Tags
Unknown
References
distclean-git-clean