> This fixes a typo I noticed. > > Ordinarily I would just check this in as obvious, but I wasn't sure > whether there was some additional process for modifications to the > docs. Is there something? Or is this ok as is? It is ok, don't worry. Many thanks, Paolo