We'll soon get a tool to automatically open PRs to update this repo.
So, we make GitHub auto assign us so we get notified.

I'll probably be the one merging these PRs most of the time,
but also adding jba to review when I'm on vacation
(or under a bus).

Eventually we'll want to automatically merge regeneration PRs,
at which point this file will probably become obsolete.