diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 2b8a22fe7c625718139bb778908499fce698eb32..9318f4ebd96b2ac41ec54496917cada92b455504 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -1480,12 +1480,12 @@ let diff_check_exist old_file new_file = if Sys.file_exists new_file then begin !do_diffs ^ " " ^ old_file ^ " " ^ new_file end else begin - "echo \"" ^ new_file ^ " does not exist. Showing " ^ old_file ^ "\";" ^ - " cat " ^ old_file + "echo \"+++ " ^ new_file ^ " does not exist. Showing " ^ + old_file ^ "\";" ^ " cat " ^ old_file end end else begin - "echo \"" ^ old_file ^ " does not exist. Showing " ^ new_file ^ "\";" ^ - " cat " ^ new_file + "echo \"--- " ^ old_file ^ " does not exist. Showing " ^ + new_file ^ "\";" ^ " cat " ^ new_file end let do_diff = function