Branch 'topic/gregor/rpc' now includes:
Jfyi, this is a new feature of our git-notify script: when a git
head moves to now include commits that have already been reported
with their diffs earlier, such a summary mail is generated. This is
so that we see what's going on with a branch even if the change
doesn't include new commits (e.g., fast-forwards).
These notifications might still be a bit too noisy in the sense that
they can report cases that aren't really that interesting. But let's
see, I'm not quite sure yet what the exact definition of
"interesting cases" is.
Robin