Zulip Chat Archive
Stream: new members
Topic: personal repo
Patrick Thomas (Feb 20 2022 at 19:07):
If I want to keep my Lean3 work in a personal repo on github, should I push the entirety of the git repo that leanproject new creates to github?
Alex J. Best (Feb 20 2022 at 19:23):
Yeah thats the recommended way to go
Patrick Thomas (Feb 20 2022 at 19:41):
Cool. Thank you.
Last updated: Dec 20 2023 at 11:08 UTC