diff options
Diffstat (limited to 'debug/DebugInit.ml')
| -rw-r--r-- | debug/DebugInit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 462ca2d3..b3fedb00 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -60,7 +60,7 @@ let init_none () = implem := default_implem let init () = - if !Clflags.option_g && Configuration.advanced_debug then + if !Clflags.option_g then init_debug () else init_none () |