No mails on merges. Can we have them?

[Aidan Kehoe]

 Ar an ceathrú lá déag de mí Bealtaine, scríobh 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. 

Not in practice; cf.
http://mid.gmane.org/18782.13793.972880.403900@parhasard.net , and I dealt
with something similar reported by Vin in the last six months, which I’m
having more trouble finding in my archives.

 > 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.)

I don’t know what the buildbot pulls. Mats?

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

-- 
“Apart from the nine-banded armadillo, man is the only natural host of
Mycobacterium leprae, although it can be grown in the footpads of mice.”
  -- Kumar & Clark, Clinical Medicine, summarising improbable leprosy research