On Tue, Feb 28, 2012 at 11:07:50PM +0000, Joseph S. Myers wrote: > I think in general it should be done in the same commit as the patch, and > only updated separately if we forget to do it with the patch. Note that in these cases we could use git commit --amend. Marek