> A problem with the policy "trivial things can just be pushed" is
> that "trivial" is open for interpretation.
Of course, but this shouldn't be a hindrance.
> Even a change that was intended to affect only comments could have a
> bad impact if, say, it inserts an accidental stray character and is
> not tested sufficiently.
I think that the benefit of having the stuff immediately in the
repository outweights the potential danger of breaking compilation.
Usually, a hotfix is a matter of seconds.
> James' report demonstrates that even if multiple devs agree that a
> change is trivial, it should still be tested before being pushed.
Well, this particular issue was *not* tagged as trivial, since it adds
a new regtest.
Werner
