There are quite a few sharp drops which might at first suggest that material is being deleted. When a line is edited, is that counted as deleting the old line and inserting a new line?
I’m sure that this graph would be of interest to the main users mailing list. Larry > On 24 Apr 2019, at 16:07, Lars Hupel <[email protected]> wrote: > > Recently, I've stumbled upon the tool "git-of-theseus" which can carry > out a more in-depth analysis of line changes: it also tracks how many > lines have survived. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
