On 10/06/2010 05:11 AM, Henning Westerholt
thank you for the fixes. Yes, if you update something in the doc sources, please update also the README file in the repository. You can of course batch several changes together.
Thanks Henning; I did not know whether that was the custom here. Certainly, it makes more sense to put many trivial doc changes into one commit, but I thought maybe because they affect different modules it is preferred to keep them separate. Certainly, I will follow the prevailing practice here.