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
I have nevertheless two suggestions:
- we could have a nightly compilation and spam pg-devel when
- we could add
to Makefile and have a LocalMakefile that makes ``check'' the
default compilation target and omit LocalMakefile from the
If you think these compilation errors are an issue, I volunteer
to implement one or both suggestions.
ProofGeneral-devel mailing list