Stream: new members
Eric Wieser (Jul 21 2020 at 08:01):
What's the preferred workflow for making a small change to mathlib? Can I work within the
_target/deps/mathlib directory of an existing project? Or should I make a clean checkout? Is there anything special I have to do to get the oleans?
Johan Commelin (Jul 21 2020 at 08:03):
Does #contrib help?
Johan Commelin (Jul 21 2020 at 08:04):
In particular https://www.youtube.com/watch?v=Bnc8w9lxe8A
Eric Wieser (Jul 21 2020 at 08:17):
That's what I was looking for, thanks. Couldn't see the
contributing.MD in the main repo, but forgot to look in
Last updated: May 14 2021 at 07:19 UTC