[DrJava] Documentation Documentation

[Peter C. <cen...@cm...>]

Hi all,

I'm interested in tweaking some of the DrJava documentation, 
specifically as regards recently added/changed features from this 
summer's work.  However, I haven't the foggiest clue how to do that.  I 
don't even remember what format the docs are originally authored in 
(DocBook maybe?).  If someone who knows (perhaps only Charlie) could 
whip up a quick section on editing the docs (what software is needed, 
how to generate the HTML and PDF) and put it in the developer docs 
online, I would appreciate it much.

--
Peter