Also, is there a way to take a PR against master and apply it as a
branch?
I generally do that by taking the PR as a patch, then applying the
patch on a branch.
But it looks like you can do that with github:
https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/changing-the-base-branch-of-a-pull-request
We will need to experiment with that, but if it works then we could
continue to use the dev branch with no PR problems. If we get a PR on
master, we could just change the base to dev.
That, of course, depends on keeping dev fairly clean and freshly rebased
to master. If things are going to linger on dev, we should move them to
another branch.
