Julian Foad wrote: > Daniel Sahlberg wrote: >> Should the following lines also be removed [...] > Oh yes. Thank you. Please do if you have a moment, otherwise I'll get > to it some time this week.
I got to it now. r1898535. I note that we might want to replace that with a matcher for variations of the new style, but I saw there didn't seem to be a trivial way to do so at the moment, and it can wait, so I didn't. Thank you very much for reviewing these commits. Please keep it coming! - Julian
