More GitHub labels

[Dr. Matthias St. Pierre]

> Your suggestion seems workable too.  PRs are merged with outstanding change requests indicated
> — a reviewer comments, the comments are addressed then a different reviewer approves without
> the original review being removed.  The labels are a bit more in your face.  A hybrid “hold: required changes see review/comments” might be workable.

GitHub can be configured to require approval. It then gives a clear visual indication that the PR is
not ready to be merged, and the Merge button is greyed out. This should be obvious enough,
even more obvious than a label, which can also easily be ignored.

Of course, our merge procedure circumvents the merge button, I'm only talking about the visual
indicator. Alternatively, the pre-receive-hook on the git.openssl.org server could enforce the policy
by checking the  reviewer state via GitHub API queries.

Matthias