doc: add hint about restarting computer.

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.

https://leanprover-community.github.io/

MIT License

51 stars 119 forks source link

doc: add hint about restarting computer. #488

Closed joneugster closed 2 months ago

joneugster commented 2 months ago

Add a hint about alternatively just restarting the computer.

joneugster commented 2 months ago

This comes from a Zulip thread where a Windows user got stuck trying to call source ~/.bash_profile on their Windows machine. Restarting is completely over-the-top, but might be simple enough and easy to understand.