If this "ambiguous" name causes trouble, we could delete it.
I've just deleted the branches 1.3.7 and 1.3.8. I could not do it via "git push github :1.3.7", because same name for tag an branch forbid me to do it. I had to go to the github website. Waldek, maybe next time, you create this temporary branch as "v1.3.9" (at least something differen from the pure number tag.
OTOH I do not feel good about "rewriting history" in such way...
I do not think that this is a big problem. Important are the sha1's and the content in the repository, but branch names are not. If you have never publicly referred to a branch name, it there is not trace in history at all.
Actually you could call a temporary branch like "wip/something". I take the position that Work-in-progress branches can be rebased or even completely deleted. The "wip/" in the branch name should make everybody aware that the branch contains something that might suddenly disappear, so you shouldn´t rely on it. Having such branches is sometimes quite nice in order to collaborate temporarily on a feature.
Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/455530d4-a214-2faa-052e-a93318b9d864%40hemmecke.org.
