From df7e8f9569e81660610eefed8cf9ffa4971bd67b Mon Sep 17 00:00:00 2001 From: Lukasz Stafiniak Date: Sun, 18 Feb 2024 21:15:34 +0100 Subject: [PATCH] Flush before reading out from a file --- minidebug_runtime.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/minidebug_runtime.ml b/minidebug_runtime.ml index a9e7573..bdac26c 100644 --- a/minidebug_runtime.ml +++ b/minidebug_runtime.ml @@ -90,7 +90,10 @@ let debug_ch ?(time_tagged = false) ?(elapsed_times = elapsed_default) current_snapshot := 0); !current_ch - let snapshot_ch () = current_snapshot := pos_out !current_ch + let snapshot_ch () = + flush !current_ch; + current_snapshot := pos_out !current_ch + let reset_to_snapshot () = seek_out !current_ch !current_snapshot let time_tagged = time_tagged let elapsed_times = elapsed_times @@ -810,7 +813,11 @@ let debug ?debug_ch ?(time_tagged = false) ?(elapsed_times = elapsed_default) let current_snapshot = ref 0 let snapshot_ch () = - match debug_ch with None -> () | Some _ -> current_snapshot := pos_out ch + match debug_ch with + | None -> () + | Some _ -> + flush ch; + current_snapshot := pos_out ch let reset_to_snapshot () = match debug_ch with @@ -841,7 +848,11 @@ let debug_flushing ?debug_ch ?(time_tagged = false) ?(elapsed_times = elapsed_de let current_snapshot = ref 0 let snapshot_ch () = - match debug_ch with None -> () | Some _ -> current_snapshot := pos_out ch + match debug_ch with + | None -> () + | Some _ -> + flush ch; + current_snapshot := pos_out ch let reset_to_snapshot () = match debug_ch with