# 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