Appending .jar to file name when generating custom DrJava.
Authored by: mgricken 2010-06-14
Parent: [r5284]
Child: [r5286]
