leanproject get fails with "Git command failed"

Stream: general

[Scott Morrison]

$ leanproject get Ruben-VandeVelde:complex-hahn-banach
Cloning from git@github.com:leanprover-community/Ruben-VandeVelde.git
Git command failed

Does anyone else see this? Am I doing something wrong?

[Gabriel Ebner]

The error message could be better, it should say "repository does not exist".

[Gabriel Ebner]

You want this:

leanproject get Ruben-VandeVelde/mathlib:complex-hahn-banach

[Scott Morrison]

Ah, of course. I was just copying and pasting the string that the Github PR displays

[Patrick Massot]

It makes me think it would be nice to decide something about https://github.com/leanprover-community/mathlib-tools/pull/65 and update leanproject before the workshop. Does anyone has an opinion here?