Should we start pushing commits with Gerrit changeset IDs? Or is it sufficiently unlikely that we will adopt Gerrit that at this point, we'd just pollute the Git history pointlessly? Thanks, Florian