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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
