How to delete files and directories from git commit history?

[Steve Litt <slitt@troubleshooters.com>]

Hi all,

I have git 2.17.1 running on Void Linux 64 bit running the Linux
4.16.9_1 kernel, not available to the public in any way (yet). I have a
repository in my project's working directory, and push to a bare
repository on the hard disk.

My project (call it myproject) had a directory (call it docs/propdir)
that was unnecessary for the project, and I've decided I don't want to
offer the files in that directory as free software. So I need to delete
docs/propdir from all commits in the repository. I did the following,
while in my working repository's myproject directory:

git filter-branch --tree-filter 'rm -rf docs/propdir' HEAD

After that command, I could git clone the working repo and then git
checkout to a commit stage that used to have the directory and files,
and they're not there. So far, so good.

But then I view all filenames from that directory that have ever been
in the project, as follows:

git cat-file --buffer --batch-all-objects \
 --batch-check='%(objecttype) %(objectname)' \
 | grep ^c | cut -d " "  -f 2 \
 | xargs -n 1 git ls-tree -r | sort | uniq \
 | grep propdir

The preceding command lists directory docs/propdir and all the files
it's ever contained. This makes me uneasy because if the filenames are
still there, I wonder if there's a route to get the files with a git
command. Second, I'd prefer that when my repo is exposed to the public,
people not know this directory and these files ever existed.

What command do I do to remove all mention of doc/propdir and its
files from my git history?

Thanks,

SteveT

Steve Litt 
June 2018 featured book: Twenty Eight Tales of Troubleshooting
http://www.troubleshooters.com/28