# HG changeset patch
# User boehmes
# Date 1256300556 -7200
# Node ID ccefc096abc9d79f28d6d740fe1c313603227f1f
# Parent  fe29679cabc23a34bebb7e8ca6a25928d7720260
ignore error messages produced by ATPs

diff -r fe29679cabc2 -r ccefc096abc9 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- 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");