> The only thing you should have done differently is push this commit
> separately from the rest

If this restriction is to workaround deficiencies of mailing
notifications, then I understand. But I don't see why pushing multiple
local commits at once would be necessarily wrong going forward.