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

[Peter Wang]

On Mon, 18 Jul 2022 15:42:47 +1000 Julien Fischer <jfischer at opturion.com> wrote:
> 
> Hi Peter,
> 
> On Mon, 18 Jul 2022, Peter Wang wrote:
> 
> > On Sun, 17 Jul 2022 17:04:37 +1000 Julien Fischer <jfischer at opturion.com> wrote:
> >>
> >> For review by anyone.
> >>
> >> Question: should the new variable in the launcher scripts be named
> >> JAVA_OPTS or JAVA_FLAGS (or something else)?
> >
> > Or *_OPTIONS?
> 
> I've seen all three suffixes in the wild.
> 
> > 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.

That's probably for the best.

Peter