From 9aa2df835e06cb49ba6381cef62b8aa137aad9c2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 12:15:05 +0000 Subject: [PATCH] avoid duplicates --- matita/matitadep.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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))) ;; -- 2.39.2