|
| From: | Karl Berry |
| Subject: | Re: info files deleted by "make" |
| Date: | Mon, 24 Feb 2003 11:16:07 -0500 |
any chance that when makeinfo succeeds it also
removes old *.info-* files that are no longer part of a manual
(e.g., after the manual has shrunk by a few files)?
Ok. (Not going to happen soon, though.)
| [Prev in Thread] | Current Thread | [Next in Thread] |