Instructions for visitors of my project

Stream: new members

[Martin Dvořák]

Can you please check I wrote instructions for visitors of my project correctly?
https://github.com/madvorak/grammars
Screenshot of the relevant part: image.png

[Johan Commelin]

You can shorten the leanproject instruction to leanproject get username/reponame

[Martin Dvořák]

Is it all right if the following happens?

$ leanproject get madvorak/grammars
Cloning from git@github.com:madvorak/grammars.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/madvorak/grammars.git
configuring grammars 0.1

[Ruben Van de Velde]

Yeah, I'm guessing that's fine