# HG changeset patch
# User blanchet
# Date 1300873130 -3600
# Node ID 217a1b61d42d34fc9b898e7ec2cfa751d2582a89
# Parent  1492ee6b8085b7e7169e0cae0904b2332b429b2f# Parent  d3404f32328a1f91dfdc884f1a329cb14b7eb2e4
merge

diff -r 1492ee6b8085 -r 217a1b61d42d src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Mar 23 10:18:42 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Mar 23 10:38:50 2011 +0100
@@ -127,16 +127,18 @@
 close(LOG_FILE);
 
 my $quiet = "";
+my $output_log = 1;
 if (defined $be_quiet and $be_quiet ne "") {
   $quiet = " > /dev/null 2>&1";
+  $output_log = 0;
 }
 
-print "Mirabelle: $thy_file\n" if ($quiet ne "");
+if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
-print "Finished:  $thy_file\n" if ($quiet ne "");
+if ($output_log) { print "Finished:  $thy_file\n"; }
 
 
 # cleanup