# Attention!

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