[m-rev.] for post-commit review: fix Mantis bug #522

[Julien Fischer]

Hi Zoltan,

On Fri, 9 Oct 2020, Zoltan Somogyi wrote:

> For review and testing by Julien.

Thanks for that; the diff looks fine and lib__optimization_options.java
now gets through the Java compiler.

There's at least one other spot where we are still exceeding the limit

    Making Java class files
    Mercury/javas/jmercury/libs__handle_options.java:3473: error: code too large
    convert_options_to_globals_24_p_0(

Julien.