git bash problem

Stream: new members

[haoyuan]

When I install the elan, the Git Bash writes" Could not resolve host: raw. githubusercontent.com". What should I do next?

[Scott Morrison]

Can you show us the entire command line and entire output? I'm not immediately sure what could be wrong.

[haoyuan]

图片.png

[haoyuan]

OK, I successfully install lean.

[Johan Commelin]

@haoyuan Glad to hear that your problem is now solved. Do you know what was wrong? Is there something that we should change / point out in the installation instructions?

[haoyuan]

@Johan Commelin I first typed the command in Git Bash, then it goes as the picture. But then I pasted the command and it worked. I don't know where I typed the wrong character.