Unable to intall mathlib4

Stream: mathlib4

[CrazyTom]

Hi everyone, I am trying to use VS code to install the mathlib project, but it seems like VS code can not access its github repository. Anyone knows how to solve the problem?

[Kevin Buzzard]

Switch your firewall off?

[CrazyTom]

Thanks for your advise. It has been done.

[Kenny Lau]

(as always, caution is needed when using AI) i've found that in situations like this (i.e. tech debugging), copying the error message to GPT has been helpful (don't copy any passwords or personal details, of course)