On 13 August 2012 12:57, Marc Glisse wrote: > I only modified the xml version. I expect the html version will be updated > the next time someone who knows what they are doing touches the doc...
That's no problem, I tend to regenerate the html fairly frequently. Thanks.