Zulip Chat Archive

Stream: new members

Topic: git bash problem

haoyuan (Apr 19 2023 at 02:49):

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

Scott Morrison (Apr 19 2023 at 02:49):

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

haoyuan (Apr 19 2023 at 02:54):


haoyuan (Apr 19 2023 at 04:53):

OK, I successfully install lean.

Johan Commelin (Apr 19 2023 at 05:47):

@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 (Apr 20 2023 at 04:11):

@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.

Last updated: Dec 20 2023 at 11:08 UTC