From 8aae10b50b321cfcbde86582cdd7ce1df8960628 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 2 Feb 2015 09:14:10 +0100
Subject: Starting to remove the seperate printers for each backend.

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

(limited to 'common/Sections.mli')

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