From a479c280441b91007c379b0b63b907926d54f930 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Oct 2015 16:23:20 +0200 Subject: Changed the type of the debug sections with additional string. Instead of using a string they now take an optional string, which should be none if the backend is not the diab backend and the corresponding section is the text section and Some s with s being the custom section name else. Bug 17392. --- common/Sections.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'common/Sections.ml') diff --git a/common/Sections.ml b/common/Sections.ml index 70311d4e..0910f2dc 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -28,9 +28,9 @@ type section_name = | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) | Section_debug_abbrev - | Section_debug_info of string + | Section_debug_info of string option | Section_debug_loc - | Section_debug_line of string + | Section_debug_line of string option | Section_debug_str type access_mode = -- cgit