diff options
| -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 e0c435cd..6a50b020 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -74,7 +74,7 @@ let init_none () = implem.exists_section <- (fun _ -> true) let init () = - if !Clflags.option_g then + if !Clflags.option_g && Configuration.advanced_debug then init_debug () else init_none () |