[isabelle-dev] More accurate AFP statistics

[Lawrence Paulson]

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 <hupel at in.tum.de> 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.