From 711cea9fc37e777487abc815730aacde2b00aef3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 28 Jun 2016 17:04:56 +0200 Subject: 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 --- driver/Optionsprinter.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'driver/Optionsprinter.ml') 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}" -- cgit