From d7bd846a248b077ac05dbb22bf21aad76bed986b Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 31 Mar 2020 11:48:12 +0200 Subject: [PATCH] [ptests] Do not count as success presence of err file without oracle More precisely, increase the number of total comparisons but not of Ok ones in that case. --- ptests/ptests.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 64401651909..2b8a22fe7c6 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -1363,6 +1363,8 @@ let check_file_is_empty_or_nonexisting diff ~log_file = 0 else begin lock(); + (* signal that there's a problem. *) + shared.summary_log <- shared.summary_log + 1; Queue.push diff shared.diffs; Condition.signal shared.diff_available; unlock(); @@ -1531,7 +1533,6 @@ let do_diff = function let diff_string = diff_check_exist oracle_file result_file in ignore (launch diff_string) - let diff_thread () = lock () ; while true do -- GitLab