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 _______________________________________________ lilypond-devel mailing list lilypond-devel@gnu.org https://lists.gnu.org/mailman/listinfo/lilypond-devel
