diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-29 16:02:56 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-29 16:02:56 +0200 |
| commit | 4e0ffb627524e3a251ee9e82ed88e1ed45e26b16 (patch) | |
| tree | 7531077fcb6112fb0b4a71b19485b4bb4860862f /debug | |
| parent | 68ad5472a78d12e0e4fd4eae422122185403d678 (diff) | |
| download | compcert-kvx-4e0ffb627524e3a251ee9e82ed88e1ed45e26b16.tar.gz compcert-kvx-4e0ffb627524e3a251ee9e82ed88e1ed45e26b16.zip | |
Deactivate the debug functions for none advanced targets.
Diffstat (limited to 'debug')
| -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 () |