Re: Problem with make

[Graham Percival]

On Thu, Sep 22, 2011 at 11:44:29AM +0200, Reinhold Kainhofer wrote:
> 
> Exactly. Make copies the *.texi file from the source to the build dir, runs 
> extract-texi-filenames.py and then removes it again...

Ouch.  Is there any compelling reason to
1) not run extract-texi-filename.py on the original file,
or
2) not remove the file?  I mean, it's not like a small text file
is going to change our 1.5 Gb build directory much.

Cheers,
- Graham