10 Feb
2014
10 Feb
'14
7:09 p.m.
It does look like a leftover. This change appears to be merged to master, and does show up in the list of commits to master:
https://github.com/boostorg/config/commits/master?page=3
but the file is still there. It should probably be deleted.
Done. Not sure why it wasn't removed by the git merge? That's a little worrying. John.