diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-12-16 17:08:13 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-12-16 17:08:13 +0100 |
| commit | eb27f1f3670b95f30c5bfbf08e05f7bb95cbdb22 (patch) | |
| tree | 25f189fb719481b3abe8d5f7723b1141d0fc2f5e | |
| parent | 54f781cd0a32d2a3636eed03a67524199b700115 (diff) | |
| download | compcert-kvx-eb27f1f3670b95f30c5bfbf08e05f7bb95cbdb22.tar.gz compcert-kvx-eb27f1f3670b95f30c5bfbf08e05f7bb95cbdb22.zip | |
Flushing at each dprintf
| -rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index dd971db8..765aa55f 100644 --- a/scheduling/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml @@ -9,10 +9,12 @@ open Lattice let debug_flag = ref false -let dprintf fmt = let open Printf in +let dprintf fmt = let open Printf in begin + flush stdout; match !debug_flag with | true -> printf fmt | false -> ifprintf stdout fmt +end let get_some = function | None -> failwith "Got None instead of Some _" |