branch_rename.sh

git pull origin master
git pull upstream master

## Make sure devel does not already exist
git branch -d devel

## Create and push the devel branch
git checkout -b devel
git push origin devel

## make devel the default branch
## https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/managing-branches-in-your-repository/changing-the-default-branch
## delete the master branch
git push --delete origin master

## push until default branch is updated on git.bioconductor.org
git push upstream devel:master

git symbolic-ref refs/heads/devel refs/heads/master