install_deps: better inform the user when github is not accessible
Opened this issue · 0 comments
JepEtau commented
It happens that github is not responding during the installation of dependencies.
- ping github before downloading the external tools
- print an error message