From a84576b219c797467e480508fc99ba78260062df Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 11 Mar 2015 18:02:36 +0100
Subject: Started integrating the debug printing in the common backend_printer.

---
 common/Sections.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common/Sections.mli')

diff --git a/common/Sections.mli b/common/Sections.mli
index be716e48..e878b9e5 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -26,7 +26,7 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
-  | Section_debug
+  | Section_debug_info
   | Section_debug_abbrev
 
 type access_mode =
-- 
cgit