New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/37315#issuecomment-1140273552

Comment:
This error also appears when running `leanproject get leanprover-community/tutorials`. Maybe the repo https://github.com/leanprover-community/tutorials has some problem...

Using `leanproject get mmasdeu/topologygame` everything works as expected. After following the steps mentioned above, opening the cloned repo in vscode and installing the lean extension, it loads the cached oleans instantly.

So I think that this package works ok.