From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Jan 2008 12:15:05 +0000 (+0000)
Subject: avoid duplicates
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=9aa2df835e06cb49ba6381cef62b8aa137aad9c2

avoid duplicates
---

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 0186a245a..fe7cab920 100644
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -169,6 +169,8 @@ let main () =
           acc d)
       [] deps
   in
-  Librarian.write_deps_file (Sys.getcwd()) (deps@List.map (fun x -> x,[]) extern)
+  Librarian.write_deps_file (Sys.getcwd()) 
+   (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x ->
+           x,[]) extern)))
 ;;