Personally, I like seeing all the commits in my git log history. Using bisect I can generally piece together what happened when. I often use the PR history, but I'd hate to not have a local copy of the history to refer to.
On Tue, Dec 14, 2021 at 3:28 PM vvs <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/4df58cd6-11fc-4530-a496-9de95f68110bn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CACKrHR8sVCymd9a26ceRUYakipCF%2BSadEKaTvyd6Nm3BcquUnQ%40mail.gmail.com.
