Re: .texi.html: Add a touch?

[Akim Demaille]

>>> "Akim" == Akim Demaille <[EMAIL PROTECTED]> writes:

 > makeinfo does not update timestamps of directories:

Is there a problem with this patch?