DrJava Mint Branch Merged Back into Trunk

I just merged the trunk-mint branch of DrJava back into the trunk and made a new weekly release (@ I actually issue these “weakly” releases more often than just weekly. It’s just a convenient mechanism to benefit from the auto-update feature. @): drjava-weekly-20090929-r5094.jar.