WARNING: bogus patch pushed

[Simon Peyton-Jones]

| Although the usual policy is not to permit "unpull"s on the main repo, I
| have unpulled this patch anyway.  If anyone (or any buildbot) has pulled
| this patch in the meantime, they should unpull it manually from their
| own repo.  I hope this does not inconvenience anyone too much.

Thanks Malcolm.  Sorry about that everyone.

| You can record an UNDO patch and push that.
|
| That should work for everyone else without them needing to take any
| action. They'll end up with both patches the 'do' and the corresponding
| 'undo' one.

I don't know how to make an UNDO patch.  But Malcolm has solved the problem anyway.

S