avoid extra subprocess -- potentially more robust on Cygwin;
authorwenzelm
Fri May 24 20:16:35 2019 +0200 (4 months ago)
changeset 702882e101846ad8f
parent 70287 b0fd8167bb9b
child 70289 85de4fdec61b
avoid extra subprocess -- potentially more robust on Cygwin;
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri May 24 20:08:52 2019 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri May 24 20:16:35 2019 +0200
     1.3 @@ -49,9 +49,8 @@
     1.4  local
     1.5  
     1.6  fun make_command command options problem_path proof_path =
     1.7 -  "(exec 2>&1;" :: map Bash.string (command () @ options) @
     1.8 -  [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
     1.9 -  |> space_implode " "
    1.10 +  Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^
    1.11 +    " > " ^ File.bash_path proof_path ^ " 2>&1"
    1.12  
    1.13  fun with_trace ctxt msg f x =
    1.14    let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()