Zulip Chat Archive
Stream: general
Topic: restarting server
Arthur Paulino (Oct 26 2021 at 20:32):
Quick question: how to restart the lean server from vs code?
Yaël Dillies (Oct 26 2021 at 20:33):
Ctrl + Shift + P and search for Restart
Patrick Stevens (Oct 26 2021 at 20:33):
Ctrl+shift+p and "Lean: Restart" action
Arthur Paulino (Oct 26 2021 at 20:34):
TYVM!
Last updated: Dec 20 2023 at 11:08 UTC