[isabelle-dev] More accurate AFP statistics

[Lars Hupel]

> 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?

This tool uses Git instead of Mercurial, which tracks content changes in 
a more fine-granular way. As far as I understand, moving lines, even 
across files, do not count as changes there. However, editing lines will 
create a +/- change.

Cheers
Lars