Merge branch 'master' into mike
authorMike Taylor <mike@indexdata.com>
Mon, 11 Aug 2014 09:19:43 +0000 (10:19 +0100)
committerMike Taylor <mike@indexdata.com>
Mon, 11 Aug 2014 09:19:43 +0000 (10:19 +0100)

Trivial merge