Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned: avoid redundant white space;
authorwenzelm
Mon, 20 Feb 2023 21:47:25 +0100
changeset 77320 7a6fa60298cd
parent 77319 87698fe320bb
child 77321 cf6947717650
tuned: avoid redundant white space;
src/Pure/ML/ml_process.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML/ml_process.scala	Mon Feb 20 21:40:52 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Mon Feb 20 21:47:25 2023 +0100
@@ -117,9 +117,9 @@
     bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
     bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
 
-    Bash.process(
-      options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
-        Bash.strings(bash_args),
+    val policy = options.string("ML_process_policy") match { case "" => "" case s => s + " " }
+
+    Bash.process(policy + """"$ML_HOME/poly" -q """ + Bash.strings(bash_args),
       cwd = cwd,
       env = bash_env,
       redirect = redirect,
isabelle