src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 49547 c0f44941e674
parent 49407 ca998fa08cd9
child 49671 5caa414ce9a2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 10:48:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -775,9 +775,9 @@
     1.4              val args = arguments ctxt full_proof extra slice_timeout
     1.5                                   (ord, ord_info, sel_weights)
     1.6              val command =
     1.7 -              File.shell_path command0 ^ " " ^ args ^ " " ^
     1.8 -              File.shell_path prob_file
     1.9 -              |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
    1.10 +              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
    1.11 +              File.shell_path prob_file ^ ")"
    1.12 +              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
    1.13              val _ =
    1.14                atp_problem
    1.15                |> lines_for_atp_problem format ord ord_info