# HG changeset patch
# User blanchet
# Date 1283161163 -7200
# Node ID ec417f7480644446342ba146d54e546f1efacb0a
# Parent  e85263e281bebc7e765de6ed741a078c3611d5cb
deal with duplicates

diff -r e85263e281be -r ec417f748064 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 30 11:11:10 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 30 11:39:23 2010 +0200
@@ -51,7 +51,11 @@
 }
 my $tools = "";
 if ($#action_files >= 0) {
-  $tools = "uses " . join(" ", @action_files);
+  # uniquify
+  my $s = join ("\n", @action_files);
+  my @action_files = split(/\n/, $s . "\n" . $s);
+  %action_files = sort(@action_files);
+  $tools = "uses " . join(" ", sort(keys(%action_files)));
 }
 
 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";