steps to delete a copyrighted file from a git repository using BFG-repo-cleaner

gistfile1.txt

# my local copy of the offending repo was at ~/github/nlesc/enram

# =================  stage 1  =================
# (I removed offending files with git rm, then commited and pushed to GitHub)

# key thing is: the HEAD needs to be clean of offending files
# I also cut all branches except master, not sure how that affects anything

# also important: merge any open pull requests, otherwise you end up undoing the
# history deletion when you merge them later

# =================  stage 2  =================
# create a *mirror* clone in a new directory
cd ~/tmp
# cloning with https is apparently important (I didn't try with git@github.com:NLeSC/enram.git)
git clone --mirror https://github.com/NLeSC/enram.git
# don't cd into it...yet

# download BFG-repo-cleaner from here: https://rtyley.github.io/bfg-repo-cleaner/
# BFG comes in the form of a jar, so to run it, you'll need Java Runtime

# for simplicity I made a bash_alias in ~/.bash_aliases:
# bfg='java -jar <path to bfg.jar>'
# (open new terminal in order to use new alias)

# BFG retroactively deletes files by filename, so if 'Chapter09.pdf' is the offending file:
bfg --delete-files Chapter09.pdf enram.git
# Note: if you happen to have (had) a file named 'Chapter09.pdf' some place else in the 
# directory tree, I assume BFG's filename-based matching will result in deletion of 
# those files as well, which may not be what you want.

# now cd into the repo
cd enram.git

# do some git magic (not entirely sure what this does, but it takes a while to complete):
git reflog expire --expire=now --all
git gc --prune=now --aggressive

# push the repo with changed history
git push 

further reading:

• https://help.github.com/articles/removing-sensitive-data-from-a-repository/
• https://rtyley.github.io/bfg-repo-cleaner/