diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/DebugPrint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index 64efe727..5078f727 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -5,7 +5,7 @@ open Registers let debug_flag = ref false let debug fmt = - if !debug_flag then (flush stderr; Printf.eprintf fmt) + if !debug_flag then (flush stderr; flush stdout; Printf.eprintf fmt) else Printf.ifprintf stderr fmt let print_ptree_bool oc pt = |