Zulip Chat Archive

Stream: new members

Topic: Searching in VS Code


view this post on Zulip 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!

view this post on Zulip Johan Commelin (Aug 24 2020 at 16:56):

Click on the little cog :settings: in the search panel

view this post on Zulip Johan Commelin (Aug 24 2020 at 16:56):

Ooh, you need to click on the three dots first

view this post on Zulip Ashvni Narayanan (Aug 24 2020 at 16:58):

Ah, it works, phew. Thank you!


Last updated: May 09 2021 at 19:11 UTC