]> matita.cs.unibo.it Git - helm.git/commitdiff
avoid duplicates
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Jan 2008 12:15:05 +0000 (12:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Jan 2008 12:15:05 +0000 (12:15 +0000)
matita/matitadep.ml

index 0186a245a44269bb1f0f7227ee9bd866566cf0e4..fe7cab92075ee99c3dd74bfe57d71934e4cbbb99 100644 (file)
@@ -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)))
 ;;