David Aspinall <david.aspin...@ed.ac.uk> writes: This fix was helpful but unfortunately means that developers are more likely to introduce bugs unless they run
make clean; make check I agree. But even before the change we had now and then compilation errors in the repository. >From my point of view the compilation errors are not an issue. They are rare and if one is reported on this list it is fixed immediately. I have nevertheless two suggestions: - we could have a nightly compilation and spam pg-devel when errors occur - we could add -include LocalMakefile to Makefile and have a LocalMakefile that makes ``check'' the default compilation target and omit LocalMakefile from the distribution. If you think these compilation errors are an issue, I volunteer to implement one or both suggestions. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel