Zulip Chat Archive

Stream: general

Topic: Rebuilding oleans

Meow (Jan 13 2023 at 07:55):

How to rebuild olean files when I changed some files in mathlib? I tried lean --make and it will rebuild the whole mathlib library, and not only the files I changed.

Johan Commelin (Jan 13 2023 at 08:03):

lean --make some/specific/file.lean

Meow (Jan 13 2023 at 08:04):

Thanks, that works.

Last updated: Dec 20 2023 at 11:08 UTC