Zulip Chat Archive

Stream: general

Topic: olean files in VSCode

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.

Bryan Gin-ge Chen (Feb 25 2020 at 06:34):

They're hidden by default. See here.

Donald Sebastian Leung (Feb 25 2020 at 06:35):

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

Last updated: Dec 20 2023 at 11:08 UTC