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