Re: How to avoid the double execution of a make info call?

[SF Markus Elfring]

> Your Makefile looks likely to rebuild .depend, a file that it includes.
> So, like Paul said:
>>> or else make has re-executed itself
>>> because this makefile or one of its 
>>> included files was rebuilt;

Yes. - This can happen at the moment.


> I wonder about the information “Re-executing[1]: make --no-builtin-rules -d” 
> there.
> Unfortunately, I do not recognise so far which rule triggers this action.
> 
> Which condition checks should I add?

I imagine that my extra information display might be useful.
Should I check anyhow then if the included dependency file was modified?

Or is it more desirable to deactivate the message “modules without mli files”?

Regards,
Markus