From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 19 Feb 2009 13:13:14 +0100
Subject: Imported Upstream version 8.2-1+dfsg

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

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index 9f3478f0..0e1342f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -629,6 +629,8 @@ let error_recursively_dependent_library dir =
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
+(* Security weakness: file might have been changed on disk between
+   writing the content and computing the checksum... *) 
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
   let md = { 
-- 
cgit v1.2.3