# HG changeset patch
# User krauss
# Date 1300715219 -3600
# Node ID 626fcf4a803ef55faf7d9ef6ee1f16fd572c243b
# Parent  1571fde21911a172e7da86a72f5538f1a659334d
fixed perl error

diff -r 1571fde21911 -r 626fcf4a803e src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:37:10 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:46:59 2011 +0100
@@ -31,7 +31,7 @@
   $end_line = $3;
 }
 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
-my $rand_suffix = map { ('a'..'z')[rand(26)] } 1 .. 10;
+my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
 my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
 my $new_thy_file = $path . "/" . $new_thy_name . $ext;