If the toplevel .depend file does not exist, a 'make depend' is automatically run prior to any other 'make' command.
I wonder that this file has got an explicit check for its existence.
Therefore, I would actually be in favor of having the 'make clean' remove all .depend files.
Would it be useful to add the dependency "*.mli *.ml" to the build target "depend"? Regards, Markus _______________________________________________ Cocci mailing list [email protected] http://lists.diku.dk/mailman/listinfo/cocci (Web access from inside DIKUs LAN only)
