# devices.xml is generated from devices.txt
/devices.xml
# devices-linux.xml is generated from devices-linux.txt
/devices-linux.xml
# *.html are generated from *.xml
/*.html