../../texmf-dist/scripts/texdef/texdef.pl