git and leanproject

Stream: new members

[Thorsten Altenkirch]

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?

[Alex Peattie]

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

[Patrick Massot]

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