Zulip Chat Archive

Stream: general

Topic: olean files in VSCode


view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 06:20):

Quick question: does VSCode display .olean files in the Explorer by default? I've included pre-compiled .olean files for mathlib in my current Lean project but when I open my Lean project in Explorer, I only see .lean files in my mathlib.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 06:34):

They're hidden by default. See here.

view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 06:35):

Okay thanks, I thought my computer was going haywire :rofl:


Last updated: May 11 2021 at 14:11 UTC