This will take you 2 minutes, so please do this as soon as you first
open this email.
While working on adding Farsi to the website, I inadvertently pushed a
big branch with tons of noise to the Git repo. I'd like to prevent this
noise to remain on it forever. I already deleted the branch remotely,
but it would also be helpful if you could delete it locally to prevent
it from being pushed again by mistake.
So please execute on your local repo:
git branch -D web/10400-farsi
You might get "error: branch 'web/10400-farsi' not found." if you had no
such branch locally.
If you had such a branch locally and have a personal remote repo, please
also execute:
git push $myrepo --delete web/10400-farsi
Where '$myrepo' is the name of your remote personal repo in your config.
And then
git fetch --prune $officialrepo
Where '$officialrepo' is the name of the official repo in your config.
Thanks!
