The file names for the documentation changed when the docs build
process was migrated to xsltproc in revision 4712, and the names were not updated in the DrJava code base.
Authored by: mgricken 2009-04-16
Parent: [r4904]
Child: [r4906]
