aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-06-28 17:04:56 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-06-28 17:04:56 +0200
commit711cea9fc37e777487abc815730aacde2b00aef3 (patch)
treef9480756132b098cb42d9853a5a188fdb156c697 /debug
parent56a6795d82c5ff0af78872a3e807b48c556ce5fe (diff)
downloadcompcert-kvx-711cea9fc37e777487abc815730aacde2b00aef3.tar.gz
compcert-kvx-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')
-rw-r--r--debug/DebugInit.ml2
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 ()