make clean should delete helper files about unimath HOT 5 CLOSED

Note that git clean -x will remove untrackted files too (git clean -X will remove only the untracked files).

from unimath.

On 12/07/2014 12:38 PM, Jason Gross wrote:

Note that git clean -x will remove untrackted files too (git clean -X will remove only the untracked files).

Thanks for the hint.
I would still prefer a more fine-grained solution via make, in order to
avoid deleting untracked Coq files by accident.

from unimath.

Once one of the makefiles that make reads has a syntax error in it, make will always refuse to
do anything. So the only way to get make to do something is to prevent it from including the
erroneous file. That can be done by adding a test for the setting of a make variable. For example,
if you had to type

    make CLEAN=yes

instead of

    make clean

would that be too counterintuitive?

Another point about git clean is that git clean -Xdfq is that the -X tells git to
remove just the files ignored by being mentioned in .gitignore, so it's safer than
git clean -xdfq, which might remove a file you want to keep. For me, that's a perfect
way to get cleaning done.

from unimath.

On 12/08/2014 03:27 PM, Daniel R. Grayson wrote:

Once one of the makefiles that make reads has a syntax error in it, make will always refuse to
do anything. So the only way to get make to do something is to prevent it from including the
erroneous file. That can be done by adding a test for the setting of a make variable. For example,
if you had to type
make CLEAN=yes
instead of
make clean
would that be too counterintuitive?

Another point about git clean is that "git clean -Xdfq" is that the -X tells git to
remove just the files ignored by being mentioned in .gitignore, so it's safer than
"git clean -xdfq", which might remove a file you want to keep. For me, that's a perfect
way to get cleaning done.

Ok. Instead of implementing a hack in the Makefile it is probably better
to simply add that git clean command to the README. I will do that right
now.

from unimath.

Not touching the Makefile, but adding a remark in README instead.

from unimath.