mathematics-in-lean

Stream: new members

[Victor Miller]

I'm trying to get the mathematics-in-lean to use on my mac. I have everything installed, and have successfully gotten other lean projects. However, when I do

leanproject get mathematics-in-lean

the following happens

leanproject get mathematics-in-lean
Cloning from git@github.com:leanprover-community/mathematics-in-lean.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/mathematics-in-lean.git
Username for 'https://github.com':

Why is it asking for a user name, and which one do I use?

[Bryan Gin-ge Chen]

You need to run leanproject get mathematics_in_lean (with underscores).

[Victor Miller]

Thanks. The error message leaves a bit to be desired :-).

[Bryan Gin-ge Chen]

(I'm guessing the reason it's asking for a user name is that something thinks that the 404 message could indicate that the repository is private and only visible after login.)