If a user names a jar file in their CLASSPATH with the
suffix ".JAR" in capital letters, then mjc doesn't look
at it as a jar file (and probably treats it as a
directory). A JML user submitted an example along these
lines. The javac compiler doesn't make this distinction
on case-insensitive file systems like Windows, at least.
As a workaround, it seems to suffice to just rename the
jar files in the CLASSPATH (the actual files can still
have upper case names).
But we should try to fix this.
Logged In: YES
user_id=633675
Apparently even on a case-sensitive file system like Linux,
javac recognizes .JAR (and .ZIP) as suffixes that are to be
treated specially in the CLASSPATH. So I found out how to
fix this in the sources for MJC and am testing my fix.
Logged In: YES
user_id=633675
This is fixed and will appear in the next release of mjc. Thanks for
your request.