Doing a new contribution

Stream: new members

[Xavier Xarles]

In
https://leanprover-community.github.io/contribute/index.html
it says that git clone and so on needs to be done only once. But it is not explained there what you should do after you propose a PR, it gets accepted and then merged, in order for your local branch to be merged and actualized with the most recent one, in order to start a new branch and so on.
What is the recommended way?

[Yaël Dillies]

You should git fetch; git pull on the master branch, then open new branches from the master branch.

[Henrik Böving]

You should checkout master (or whatever other branch you want to base your next piece of work on), pull it and then branch of again into a new branch of yours.

[Xavier Xarles]

Thanks! Could be a good idea to explain this in the instructions about doing a contribution...

[Eric Wieser]

Perhaps we should give instructions that work for both the first and nth contribution

[Eric Wieser]

I think git checkout -b $GITHUBNAME/$BRANCHNAME origin/master --no-track is such a command (along with general advice to run git fetch