Zulip Chat Archive

Stream: new members

Topic: git and leanproject

view this post on Zulip Thorsten Altenkirch (Oct 07 2020 at 17:18):

Ok, I have a git repo and want to use lean with math lib. Following the advice I create a leanproject which installs a local copy of math lib. Do I just add everything to my git repo or is there a more clever way to deal with this?

view this post on Zulip Alex Peattie (Oct 07 2020 at 17:40):

I think you should add _target to your .gitignore, e.g. see this example: https://github.com/b-mehta/topos/blob/master/.gitignore

view this post on Zulip Patrick Massot (Oct 07 2020 at 17:46):

No, this is automatic. He already has the relevant .gitignore.

Last updated: May 14 2021 at 12:18 UTC