From now, you can just `make userdocs' in doc, no need to use ugly scripts.
Also, `make progdocs' builds the programmer's documentation in HTML,
LaTeX version to come later.
All documentation is built in obj/doc (resp. doc/ if you do a stand-alone build).
Use `make docs' to make the whole documentation or `make userdocs' resp.
`make progdocs' for user manual resp. developer's guide.