Just in case somebody was wondering what’s going on.
I messed up and added some private data to the repo. Because of how GitHub works, the commit reference is still available in the PR.
A request has been sent to GitHub support for deletion. Once that’s fixed, I will bring back the repo and post another message here.