vere
vere copied to clipboard
master branch:
When we tried to merge @jalehman's release PR this morning, it was impossible to merge without approval from @mcevoypeter, probably because he had been assigned as a reviewer by Josh. Fortunately, for this release we were able to get Peter on the line to review it, but for the future, we should make sure that anyone on GitHub's "runtime" team can merge PRs, to prevent a release from getting delayed due to a single person not being present on release day.
I didn't assign Peter directly, that's done automatically.