Zulip Chat Archive
Stream: new members
Topic: Searching in VS Code
Ashvni Narayanan (Aug 24 2020 at 16:52):
VSCode is not showing me any of the local mathlib files in the search results. Is there anything I can do about this? Thank you!
Johan Commelin (Aug 24 2020 at 16:56):
Click on the little cog :settings: in the search panel
Johan Commelin (Aug 24 2020 at 16:56):
Ooh, you need to click on the three dots … first
Ashvni Narayanan (Aug 24 2020 at 16:58):
Ah, it works, phew. Thank you!
Last updated: Dec 20 2023 at 11:08 UTC