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 /driver/Optionsprinter.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 'driver/Optionsprinter.ml')
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index f046b40a..9dce8592 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -91,7 +91,6 @@ let print_configurations oc lib_path = p_jmember oc "stdlib_path" p_jstring lib_path; p_jmember oc "has_runtime_lib" p_jbool Configuration.has_runtime_lib; p_jmember oc "has_standard_headers" p_jbool Configuration.has_standard_headers; - p_jmember oc "advanced_debug" p_jbool Configuration.advanced_debug; p_jmember oc "struct_passing_style" print_struct_passing_style Configuration.struct_passing_style; p_jmember oc "struct_return_style" print_struct_return_style Configuration.struct_return_style; fprintf oc "\n}" |