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 see that the java launcher from JDK 9+ supports the JDK_JAVA_OPTIONS
variable so perhaps we can use that?
> --------------
>
> Improvements to the Java launcher scripts.
>
> Add new options that allow Java runtime flags to be set in the launcher scripts
> we generate for executables in the Java grade.
>
> compiler/options.m:
> Add two new options: --java-runtime-flags and --java-runtime-flag
> that can be used to embed flags for the Java interpreter in the
> launcher scripts we generate for Java grade executables.
>
> Add --javac-flags and --javac-flag as synonyms for --java-flags
> and --java-flag respectively.
>
> Rename the corresponding values of the option/0 type to
> java_compiler_flags and quoted_java_compiler_flag respectively.
>
> Extend the documentation of --java-classpath to say that it also
> affects the Java launcher scripts.
>
> compiler/module_cmds.m:
> Include any user-specified Java runtime flags in the launcher
> scripts.
>
> compiler/compile_target_code.m:
> Conform to the above change.
>
> doc/user_guide.texi:
> Document the above option changes and additions.
>
> Document how the launcher scripts interact with with the new
> options and also with --java-classpath.
>
> NEWS:
> Announce the above changes.
> @@ -924,7 +928,8 @@ write_java_shell_script(Globals, MainModuleName, JarFileName, Stream, !IO) :-
> "CLASSPATH=", ClassPath, "\n",
> "export CLASSPATH\n",
> "JAVA=${JAVA:-", Java, "}\n",
> - "exec \"$JAVA\" jmercury.", ClassName, " \"$@\"\n"
> + "JAVA_OPTS=${JAVA_OPTS:-", RuntimeOpts, "}\n",
> + "exec \"$JAVA\" $JAVA_OPTS jmercury.", ClassName, " \"$@\"\n"
> ], !IO).
RuntimeOpts should be quoted/escaped (here and elsewhere).
If options.quote_arg doesn't do it, I think the simplest method is to
wrap the value in single quotes, and replace any internal single quote
char with '\'' (i.e. close string, backslash escaped single quote,
open new string).
Peter