This is fixed in drjava-beta-20160913-225446.