author | blanchet |
Tue, 21 Dec 2010 13:57:35 +0100 | |
changeset 41361 | d1e4a20911cb |
parent 41360 | 7e82d621adc6 |
child 41362 | 3cb30e525ee9 |
--- 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 = ", "; }