OpenSees Cloud

OpenSees AMI

OpenSees GitHub

Remove a branch from the server

git branch -D branchname
git push origin :branchname # or delete at github.com after PR is merged
git remote prune origin

Copy file from branch A to branch B

git checkout branchB
git checkout branchA filename
git commit -m "Adding filename to branchB"

Force local master to be the same as upstream/master

git checkout master
git reset --hard upstream/master  
git push origin master --force