--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Oct 23 10:11:56 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Oct 23 14:22:36 2009 +0200
@@ -141,7 +141,8 @@
(* write out problem file and call prover *)
fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
- [File.shell_path cmd, args, File.shell_path probfile] ^ " ; } 2>&1"
+ [File.shell_path cmd, args, File.shell_path probfile] ^ " 2> /dev/null" ^
+ " ; } 2>&1"
fun split_time s =
let
val split = String.tokens (fn c => str c = "\n");