No mails on merges. Can we have them?

[Stephen J. Turnbull]

Mats Lidell writes:

 > It is enough if the the buildbot gets the mail. No need to bore the
 > list if that is what merge will do. 
 > 
 > (I thought merges would be interesting since, at least non trivial
 > ones, could get wrong!? And announcing that there is new stuff to pull
 > would also be interesting not only for buildbots!? But I guess I'm
 > missing something here.)

No, merges are totally boring, at least in theory.  Here's why: a
merge will only occur in practice if somebody has made a commit not
yet in the tree.  That commit will be reported to the list and trigger
the buildbot.  But what will the buildbot pull?  I assume it pulls
tip, which by the time the bot receives the trigger mail, tip will
include the merge.  (*Maybe* there's a race condition here, but I
doubt it because the mailbot collects all the commits before sending
any AIUI.)

Note that unless you use push -f, every concurrent commit will imply a
merge, as well, so we're covered in that direction too.