Seems it's not particularly easy, and that's the reason I'll be answering my own question despite many similar questions regarding git [index-filter|subdirectory-filter|filter-tree], as I needed to use all the previous to achieve this!
First a quick note, that even a spell like in a comment on Splitting a set of files within a git repo into their own repository, preserving relevant history
SPELL='git ls-tree -r --name-only --full-tree "$GIT_COMMIT" | grep -v "trie.lisp" | tr "\n" "\0" | xargs -0 git rm --cached -r --ignore-unmatch'
git filter-branch --prune-empty --index-filter "$SPELL" -- --all
will not help with files named like imaging/DrinkkejaI<0300>$'\302\210'.txt_74x2032.gif
.
The aI<0300>$'\302\210'
part once was a single letter: ä
.
So in order to extract a single file, in addition to filter-branch I also needed to do:
git filter-branch -f --subdirectory-filter lisp/source/model HEAD
Alternatively, you can use --tree-filter:
(the test is needed, because the file was at another directory earlier, see:
How can I move a directory in a Git repo for all commits?)
MV_FILTER='test -f source/model/trie.lisp && mv ./source/model/trie.lisp . || echo "Nothing to do."'
git filter-branch --tree-filter $MV_FILTER HEAD --all
To see all the names a file have had, use:
git log --pretty=oneline --follow --name-only git-path/to/file | grep -v ' ' | sort -u
As described at http://whileimautomaton.net/2010/04/03012432
Also follow the steps on afterwards:
$ git reset --hard
$ git gc --aggressive
$ git prune
$ git remote rm origin # Otherwise changes will be pushed to where the repo was cloned from