GitHub issue labels

I have introduced three new labels for GitHub issues in our repo to better
track status:

"editorial" means that the issue is editorial and the Editor will address
it by directly committing to the specification at any time.
"needs implementation" means that the issue is clear and a text proposal
(Pull Request) is needed.
"needs review" means there is a Pull Request that people should review.
"final review" means the Pull Request has been reviewed / updated (or is
uncontroversial and received no comments) and will soon be merged.

...Mark