Gavin Sinclair wrote:
> Conclusion: I prefer a configure-time option to *disable* documentation.
> 


What he said.


James