Flaw in our process for dealing with trivial changes

[Dr. Matthias St. Pierre]

> > The server-side commit hook ensures that
> >
> > - the "CLA: trivial" annotation is present in *all* commits of the PR if and only if the [cla: trivial]
> >   label is set.
> > - the [cla: ok] label is set if and only if the CLA is on file
> > - the pull request is accepted only if the [cla: ok] or [cla: trivial] label is set
> 
> 
> One issue with this bit is that it requires the git hooks to connect to
> github to check the labels. AFAIK we don't do that at present. Does it
> add too much complexity to the hooks?

Actually, the consistency checks could be done entirely by the addrev script, which already uses the GitHub API.

addrev:
=====

Ensure that

- the [cla: ok] label is set if and only if the CLA is on file
- the [cla: trivial] label is set if and only if the "CLA: trivial" annotation is present in *all* commits of the PR

git commit hook
=============

Accept pull request if and only if the CLA is on file or *all* commits have the "CLA: trivial" annotation.


(The git commit hook would need only a minimal change, if it does not check *all* commits yet.)