limbo/scripts
Pekka Enberg bd94303377 scripts/merge-pr.py: Manually map Github username to email address
You can get pretty much any old email address out of Github API, so
let's just map the emails manually.
2024-09-22 07:05:08 -04:00
..
merge-pr.py scripts/merge-pr.py: Manually map Github username to email address 2024-09-22 07:05:08 -04:00