Subject: Re: bug#7397: make-docfile should support the @FILE command line option
From: Glenn Morris <[email-masked]>
To: [email-masked]
Date: Sat, 09 Jul 2011 15:03:51 -0400
List-Id: <debbugs-submit.debbugs.gnu.org>

I don't think we need to keep this open.
The src/Makefile ugliness is hopefully reduced/gone now.