> Incompatiblity between me and git. Commit was supposed to go on > branch but went to master.
You wanted an empty commit at branch "1.3.7"? > Docs that I have give no info about removing commit, but say how one > can change it, so I changed it to empty one... Because, by default removing commits is considered bad. But of course, locally, one can do anything with his own repo. Try git reset --hard HEAD^ next time, bur first read, what that actually does. 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 fricas-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/491550eb-9284-c413-2189-d7e7ac99c151%40hemmecke.org.
