better parsing of options, in case the value has '='
authorblanchet
Tue, 21 Dec 2010 13:57:35 +0100
changeset 41361 d1e4a20911cb
parent 41360 7e82d621adc6
child 41362 3cb30e525ee9
better parsing of options, in case the value has '='
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 = ", ";
       }