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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
