DrJava branch for December 2007 beta; based on revision 4268 with changes from 4286; excluding revisions between those two.
Authored by: mgricken 2007-12-20
Parent: [r4286]
Child: [r4288]