5bb3e739ff
You do not need to run difftags.py yourself. It is a utility for keeping this repo up to date.
difftags.py