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