src/HOL/Mirabelle/lib/scripts/mirabelle.pl
changeset 38895 ec417f748064
parent 37378 5449c9aafdca
child 38898 a243f8883e8e
equal deleted inserted replaced
38894:e85263e281be 38895:ec417f748064
    49     push @action_names, $1;
    49     push @action_names, $1;
    50   }
    50   }
    51 }
    51 }
    52 my $tools = "";
    52 my $tools = "";
    53 if ($#action_files >= 0) {
    53 if ($#action_files >= 0) {
    54   $tools = "uses " . join(" ", @action_files);
    54   # uniquify
       
    55   my $s = join ("\n", @action_files);
       
    56   my @action_files = split(/\n/, $s . "\n" . $s);
       
    57   %action_files = sort(@action_files);
       
    58   $tools = "uses " . join(" ", sort(keys(%action_files)));
    55 }
    59 }
    56 
    60 
    57 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
    61 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
    58 
    62 
    59 print SETUP_FILE <<END;
    63 print SETUP_FILE <<END;