Subject: Re: bug#7397: make-docfile should support the @FILE command line option

From: Glenn Morris <[email-masked]>
Date: Sat, 09 Jul 2011 15:03:51 -0400

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