Hi,

currently editor backup files are deleted by make clean. I find
this unfortunate, because I have to use make clean quite often to
remove elc files. If nobody disagrees, I move the removal of *~
to the distclean target.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to