Oh, I should probably do this for the Tools/demo directory which I preserved in gvanrossum/old-demos. I wouldn’t feel bad at all doing a git push -f there. (I wrote many of those demos so I feel particularly motivated to preserve them somewhere other than git history.)