OpenSees GitHub
Remove a Branch from 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 Same as upstream/master
git checkout master
git reset --hard upstream/master
git push origin master --force