From 2d96b7927719c3b61fe564e8ab273a1b154912a5 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 1 Oct 2015 19:16:59 +0200
Subject: Moved the types defined by the Debug Interface into a separate file.

---
 debug/Dwarfgen.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'debug/Dwarfgen.ml')

diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 6c79ce0c..1ef00c31 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -15,8 +15,10 @@ open C
 open Camlcoq
 open Cutil
 open DebugInformation
+open DebugTypes
 open DwarfTypes
 open DwarfUtil
+
 (* Generate the dwarf DIE's from the information collected in DebugInformation *)
 
 (* Helper function to get values that must be set. *)
-- 
cgit