Commit 594e89d0 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Do not let I/O errors prevent detection of prover termination. (Fix for bug #16695.)

parent 5c2be0f2
......@@ -188,9 +188,11 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
fun () ->
if Debug.test_noflag debug then begin
if cleanup then Sys.remove fin;
if inplace then Sys.rename (save fin) fin;
if redirect then Sys.remove fout
let swallow f x =
try f x with Sys_error s -> eprintf "Call_provers: %s@." s in
if cleanup then swallow Sys.remove fin;
if inplace then swallow (Sys.rename (save fin)) fin;
if redirect then swallow Sys.remove fout
end;
let ans = match ret with
| Unix.WSTOPPED n ->
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment