# HG changeset patch
# User blanchet
# Date 1504821740 -7200
# Node ID 1eb8e87f7f8bb9306a9814bcc69fc8761a7998c3
# Parent  984c179a00d39ac379b6cf06ce0325087498fbdf
proper Bash escaping

diff -r 984c179a00d3 -r 1eb8e87f7f8b src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:16 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:20 2017 +0200
@@ -91,7 +91,7 @@
           "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
           nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
           (if specialize then "" else "--no-specialize ") ^
-          "--solvers \"" ^ Bash_Syntax.string (space_implode "," solvers) ^ "\" " ^
+          "--solvers \"" ^ space_implode "," (map Bash_Syntax.string solvers) ^ "\" " ^
           "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
           File.bash_path prob_path;
         val comments =