Zulip Chat Archive
Stream: Lean for the curious mathematician 2020
Topic: git help
Johan Commelin (Jul 15 2020 at 08:17):
So it's safe to git pull
Scott Morrison (Jul 15 2020 at 08:17):
Alternatively, you could create a new branch, say my_work
Scott Morrison (Jul 15 2020 at 08:17):
and then instead of using git pull, use git merge origin/master
Patrick Massot (Jul 15 2020 at 08:18):
And also there is no reason for you to git push
Scott Morrison (Jul 15 2020 at 08:18):
which will bring in any changes we've made to exercises
Filippo A. E. Nuccio (Jul 15 2020 at 08:20):
Ok, sure, I will never push. I was just wondering and asked to be sure. Thanks.
Last updated: Dec 20 2023 at 11:08 UTC