diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 64401651909d77b6750644327c810e154d6dce20..2b8a22fe7c625718139bb778908499fce698eb32 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