merged
authorhaftmann
Thu, 10 Jun 2010 12:28:27 +0200
changeset 37394 92a75e6d938b
parent 37386 842fff4c35ef (diff)
parent 37393 6ff1fce8e156 (current diff)
child 37395 fe6262d929a3
child 37396 18a1e9c7acb0
merged
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Jun 10 12:26:07 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Jun 10 12:28:27 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