[m-rev.] --no-line-numbers by default for us

Paul Bone paul at bone.id.au
Wed Dec 9 10:35:44 AEDT 2015

On Tue, Dec 08, 2015 at 06:54:51PM +1100, Zoltan Somogyi wrote:
> Would anyone object to committing this diff?

Is this because it will require a bootstrap?  This is fine with me.

I think that we already agreed that omitting line numbers for Mercury will
help avoid spurious recompilations.  Am I remembering correctly?

Paul Bone

More information about the reviews mailing list