5 Sep 2020 5 Sep '20
On Sat, Sep 5, 2020 at 10:25 AM Boris Epstein email@example.com wrote:
Now how do I proceed? What is the convention for Git brach names, etc?
This document should give you the steps to create a Git branch and proceed with a PR: