# HG changeset patch
# User wenzelm
# Date 1558721795 -7200
# Node ID 2e101846ad8f751ba0c6b843c226c448cbee14e1
# Parent  b0fd8167bb9b7543c4605330fe7821bec90af912
avoid extra subprocess -- potentially more robust on Cygwin;

diff -r b0fd8167bb9b -r 2e101846ad8f src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri May 24 20:08:52 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri May 24 20:16:35 2019 +0200
@@ -49,9 +49,8 @@
 local
 
 fun make_command command options problem_path proof_path =
-  "(exec 2>&1;" :: map Bash.string (command () @ options) @
-  [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
-  |> space_implode " "
+  Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^
+    " > " ^ File.bash_path proof_path ^ " 2>&1"
 
 fun with_trace ctxt msg f x =
   let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()