diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-28 17:04:56 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-28 17:04:56 +0200 |
commit | 711cea9fc37e777487abc815730aacde2b00aef3 (patch) | |
tree | f9480756132b098cb42d9853a5a188fdb156c697 /debug/DebugInit.ml | |
parent | 56a6795d82c5ff0af78872a3e807b48c556ce5fe (diff) | |
download | compcert-711cea9fc37e777487abc815730aacde2b00aef3.tar.gz compcert-711cea9fc37e777487abc815730aacde2b00aef3.zip |
Activate advanced debug information for arm, ia32.
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
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 () |