How can people best move something from targeted at master to targeted at 0.F-dev?

[actual-nh]

(Since I can't delete it, I'm asking something constructive.) This is a question for @ZhilkinSerg, or anyone else who knows:

It is reasonably clear how to start a branch as targeted at 0.F-dev in the first place, at least if one is using git command-line on Linux or Mac (instructions for other circumstances are also of interest). How does one best move a branch from targeted at master to targeted at 0.F-dev, without adding lots and lots of commits due to the differences (and requesting a lot of reviewers automatically)?

[ZhilkinSerg]

git rebase -i origin/0.F-dev I guess.

[actual-nh]

How does one change the target in github? Will that do it? (I'm guessing not.)

[ZhilkinSerg]

https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/changing-the-base-branch-of-a-pull-request

[actual-nh]

Thank you. From #47530, apparently one should do the first, and (force-)push it, before the second?

[actual-nh]

Also: From #48728, when rebasing, make sure your local copies of both master and 0.F-dev are up to date!