I also use the github website. Note that when you do your initial branch push, it displays a message in the command line that gives you the URL to open the new pr.
-- vyzo
On Mon, Nov 11, 2019 at 8:20 PM Lassi Kortela lassi@lassi.io wrote:
Could you guys share the steps that work for you? Do you use “hub”?
I just use the GitHub website. When you go to the front page for a repo where you just pushed some code, it shows a small pop-up that says "you just pushed code to branch xyz" with a "create PR" button next to it. When you click that button it takes you to a pre-filled PR creation form where you often don't need to do anything else than click OK.
"hub" is probably smarter but I find the above shortcut quite effortless. All the GitHub repos you use will be in the web browser's recently used URLs anyway, so you only need to type part of the repo's name in the address bar to go to it.
Gambit-list mailing list Gambit-list@iro.umontreal.ca https://mailman.iro.umontreal.ca/cgi-bin/mailman/listinfo/gambit-list