bad merge in staging

[Graham Percival]

We've got a mess in master now, starting with
0f68a5a1b6f789c2a0ec0e4584a3495832a3b6d7

I noticed the problem before Patchy ran, but I assumed that the
merge --ff-only  would reject the mess.  Unfortunately it didn't,
so we now have a span of a few commits that will fail to compile,
as well as some duplicated commits.

Mike, what did you do when you pushed your addition of
  5657e399609abfa2436aeec74e2498d16219e813
?  I want to find out if there were any warnings that you skipped
over, or if Patchy needs some extra checks, or what.  The whole
point of Patchy is that we should avoid this situation.

I have vague suspicions about git pull -r vs. git pull; we used to
be told to always use git pull -r but it appears that David favors
plain git pull (or rather: a combination of git fetch and
something else).  If that's the cause of this problem, let's get
the CG cleared up.

Cheers,
- Graham