Fix a mkdef.pl warning