The filenames corresponding to the manual are still manual.sgml.head and manual.sgml.tail. Shouldn't they now be manual.xml.head and manual.xml.tail? -- Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.org/> 100% accessible validated (X)HTML - Blog: <http://www.vinc17.org/blog/> Work: CR INRIA - computer arithmetic / SPACES project at LORIA