It now prints lines like: Pin("D9", mode=IN, pull=PULL_UP, GPIO=PA07) or LED("LED") showing for consistency the names as given in pins.csv. For pins, the GPIO numer is printed as well for a reference.
The names are defined in pins.csv.
The files pins.c and pins.h are generated during the build process from pins.csv, using a make-pins.py script.