2.13.18 might not contain everything

[Graham Percival]

My git history looks a bit weird (I think I forgot to push at the
right time), and a quick check indicates that the fix to 1027 (a doc
fix added a few days ago) wasn't included.

Bug squad: if you're verifying an issue and it wasn't fixed, change
the fixed_2_13_18 to fixed_2_13_19 and test it once that's out.  I'll
do 2.13.19 early next week.

Sorry about the inconvenience,
- Graham