2 Feb
2012
2 Feb
'12
11:39 a.m.
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.