> Git can handle it, but it's a lot more confusing for people looking at the > history; things like HEAD~3 go who knows where and it's difficult to see at > a glance what's going on when half of the commits are merges that clutter > up the graph. >
I should add that by default `git log` shows commits not in topo order, so they might get ordered before commits that logically should go after it. That confused me a lot sometimes, especially after merging a big PR with lots of commits and a long discussion. But yes, that's certainly "not a hill to die on" and Lean and Metamath communities are very different. -- You received this message because you are subscribed to the Google Groups "Metamath" 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/metamath/4df58cd6-11fc-4530-a496-9de95f68110bn%40googlegroups.com.
