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
  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

If you think these compilation errors are an issue, I volunteer
to implement one or both suggestions.


ProofGeneral-devel mailing list

Reply via email to