GitHub already added the feature to rename the default branch and re-target the PRs on the new default branch. @GitTools/developers do you agree with that? It will require also adapting the build scripts and maybe the code itself