From 5725e8d4ffcc9bde14b0c46fcaba83a9d84c7ddb Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 14 Nov 2014 13:42:11 +0100
Subject: More functionality for the Printer.

---
 debug/DwarfPrinter.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'debug')

diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 270e4025..0c5fc96f 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -308,6 +308,9 @@ module DwarfPrinter(Defs:DWARF_DEFS) :
 
     let print_debug oc entry =
       compute_abbrv entry;
-      print_abbrv oc
+      print_abbrv oc;
+      info_section_start oc;
+      
+      info_section_end oc
 
   end)
-- 
cgit