On 2019-09-28, Simon King <simon.k...@uni-jena.de> wrote: > I wonder what's different. I am still reluctant to do "git checkout -f ><branchname>", but perhaps that would be my best bet.
I tried, and it seemed to work. However, someone who knows about git (i.e., not I) should report the bug that git allows deletion of a branch that is checked out in another worktree. Best regards, Simon -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/qmv0tl%246eqo%241%40blaine.gmane.org.
