-
Juanma Barranquero authored
they are already deleted by the `clean' and `distclean' targets, and they are in the $(infodir) directory, not the current one.
c6883bfc
they are already deleted by the `clean' and `distclean' targets, and they are in the $(infodir) directory, not the current one.