Topic: clean up old files
Reid Barton (Jan 22 2019 at 14:21):
I wrote two Python scripts this morning to help with the transition of moving everything to
src/. One deletes
.olean files without a corresponding
.lean file, the other deletes directory trees that contain no files.
I notice @Simon Hudon also wrote an equivalent shell script in the fold PR (https://github.com/leanprover/mathlib/pull/376/files#diff-81a7c4de26bf82dac09e943b11b95792).
Windows users: is one of shell scripts/Python scripts more usable than the other?
Jeremy Avigad (Jan 24 2019 at 20:06):
BTW, I simply used
git clean -xdf to do this (
git clean -xdn will do a dry run without deleting anything).
Last updated: May 11 2021 at 23:11 UTC