# HG changeset patch
# User blanchet
# Date 1292936255 -3600
# Node ID d1e4a20911cbe1483b1c63a6051961b237c35437
# Parent  7e82d621adc651aeeacb56f34025ee292d2a6b84
better parsing of options, in case the value has '='

diff -r 7e82d621adc6 -r d1e4a20911cb src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Dec 21 13:57:19 2010 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Dec 21 13:57:35 2010 +0100
@@ -82,7 +82,7 @@
     print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
     my $sep = "";
     foreach (split(/,/, $settings_str)) {
-      if (m/\s*(.*)\s*=\s*(.*)\s*/) {
+      if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
         print SETUP_FILE "$sep(\"$1\", \"$2\")";
         $sep = ", ";
       }