If the sources are newer than the generated file, the tool (in this case 'menhir') should be invoked by the Makefile and should be required to produce a new generated file.
Are the needed dependencies completely specified in the affected build files already?
Does the configuration script need any updates eventually? Regards, Markus _______________________________________________ Cocci mailing list [email protected] http://lists.diku.dk/mailman/listinfo/cocci (Web access from inside DIKUs LAN only)
