> 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