[m-rev.] for review: improvements to the Java launcher scripts

[Peter Wang]

On Sat, 23 Jul 2022 02:10:10 +1000 Julien Fischer <jfischer at opturion.com> wrote:
> 
> On Mon, 18 Jul 2022, Peter Wang wrote:
> 
> >>> I see that the java launcher from JDK 9+ supports the JDK_JAVA_OPTIONS
> >>> variable so perhaps we can use that?
> >>
> >> We still support Java 8 (and that's not going anywhere soon). I would
> >> like to avoid the same names as the variables supported by the Java
> >> tools themselves.  How about we change all of the variables in the
> >> Mercury launchers that can be overridden to have a MERCURY_ prefix,
> >> e.g.
> >>
> >>      MERCURY_JAVA
> >>      MERCURY_JAVA_OPTIONS
> >>
> >> (There's some precedent for doing this since the shell scripts we use
> >> in the C grades have MERCURY_C_COMPILER etc.)
> >>
> >> That should reduce the risk of clashes with (a) Java itself and (b)
> >> other stuff written in Java.
> 
> The following diff does the above and addresses the other review
> comments.
> 

That looks okay.

Peter