On Tue, 18 Jul 2023 at 05:23, Aaron Meurer <asmeu...@gmail.com> wrote: > > But note that this is not a trivial thing to do, which is why it > hasn't happened yet. It's not as simple as just renaming the branch. > We also have to fix all the references to "master" everywhere, > including making sure that all our automation and release scripts > still work.
Flipping the name in Github is trivial I think. It is probably not difficult for someone experienced to fix up the workflow tooling and docs but there is a nonzero amount of work that someone would have to do. Personally I have not cared enough about this to want to spend any of my time doing it but I don't object to someone else doing it. > There's also an unfortunate downside of doing this, which is that > anyone who already has a clone of the repo and is using "git checkout > master; git pull" will have their workflows broken when master stops > being updated. I don't know if there's a clean way we can do anything > about that. This is the main reason that I have deliberately not brought this up before. It is not just a case of one person making changes in GitHub because it breaks every contributor's local clones. Our contributors waste enough time with git problems and this is adding a new one that many of them will need help with. The bulk of the work involved in doing this is probably coaching contributors on how to fix these problems. The exact way to fix it depends on how your local clone is set up as well as how you use git (I am not sure how many contributors actually use git from the command line now that various editors can do it for you). -- Oscar -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAHVvXxQhN3wbvDqXORV%3DKVhx1coAHywJ-XYH%3DCjR_KLF7p8iJA%40mail.gmail.com.
