From 7befcc7ea63ea4bd6e45e6f4b8ec01a69b586cc7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 24 Aug 2014 11:17:00 +0200
Subject: Fix Declaremods.end_library (Closes: #3536)

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

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 1ee3ca57b..f33f244b8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -313,7 +313,7 @@ let start_compilation s mp =
   comp_name := Some s;
   path_prefix := prefix
 
-let end_compilation dir =
+let end_compilation_checks dir =
   let _ =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
@@ -338,6 +338,9 @@ let end_compilation dir =
 	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
              spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
   in
+  oname
+
+let end_compilation oname =
   let (after,mark,before) = split_lib_at_opening oname in
   comp_name := None;
   !path_prefix,after
-- 
cgit v1.2.3