+../include/xbt/graphxml.h xbt/graphxml.l: xbt/graphxml.dtd
+ @echo "ERROR: src/xbt/graphxml.dtd was modified, but the flexml program was not detected"
+ @echo "ERROR: Please install it, or if you didn't modify this file, try this:"
+ @echo "ERROR: touch src/include/xbt/graphxml.h src/xbt/graphxml.l"
+ @exit 1