Seems like the both work.
I had another question regarding the links to the Documentation guide
on this node. I have just updated the guide, but now the PDF on the
site is out of sync with the documentation source.
I would think that there must be some plugin that allows drupal to
render DocBook XML in the site. Is it possible to do this?
Another possibility would be somehow to produce continuous builds of
the documentation, so that the documentation is always up to date when
linked against the site. I think this would be possible through a
relatively minor shell script.