Thanks, I've committed it. It seems like something that could be
generally useful. Just one small point: I prefer to use spaces rather
than tabs in ML and C/C++ source. Tabs cause problems with different
editors and I think now I've eliminated all of them from the Poly/ML
sources.
Regards,
David
On 29/01/2012 18:47, Florian Weimer wrote:
The patch below adds an --error-exit option and uses it in the
makefile. This avoids replacing the compiler with something that
doesn't work at all due to compilation errors.
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
