The reason for the use of `origin/master` here is probably that some other projects (sage is among them, I think), that suggest to contributors to delete `master` in their clone. `origin/master` has the advantage of working in both this and the standard scenario, but a plain `master` might be easiest to understand for those less accustomed with remote branches in git. I'm not sure which version is best, I just want to make sure you think about this before making the changes.