# HG changeset patch
# User krauss
# Date 1276164513 -7200
# Node ID 5449c9aafdca14f64325f03ff9dd4f8dcc1928a2
# Parent  e4d56f44e757490b0c5adb73d1b396a2ef9b0f23
Adapted Mirabelle script (cf. f60e4dd6d76f)

diff -r e4d56f44e757 -r 5449c9aafdca src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Jun 14 21:12:51 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Jun 10 12:08:33 2010 +0200
@@ -63,10 +63,10 @@
 begin
 
 setup {* 
-  Config.put_thy Mirabelle.logfile "$log_file" #>
-  Config.put_thy Mirabelle.timeout $timeout #>
-  Config.put_thy Mirabelle.start_line $start_line #>
-  Config.put_thy Mirabelle.end_line $end_line
+  Config.put_global Mirabelle.logfile "$log_file" #>
+  Config.put_global Mirabelle.timeout $timeout #>
+  Config.put_global Mirabelle.start_line $start_line #>
+  Config.put_global Mirabelle.end_line $end_line
 *}
 
 END