Stream: committers/git-help
Topic: what happens to my PR?
Eric Haas (Oct 13 2018 at 01:35):
I made a PR a couple of weeks ago and I assumed it went through after the build says it is OK then what? Do I merge or does somebody else do that?
Lloyd McKenzie (Oct 13 2018 at 02:18):
Once the PR-specific build succeeds you'll need to merge it yourself. @Josh Mandel are we going to be able to get auto-merge happening or was our only option that tool that messed up everyone's privileges?
Last updated: Apr 12 2022 at 19:14 UTC
