changeset 32522 | 1b70db55c811 |
parent 32521 | f20cc66b2c74 |
child 37378 | 5449c9aafdca |
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Sat Sep 05 11:45:57 2009 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Sat Sep 05 15:46:52 2009 +0200 @@ -82,6 +82,10 @@ print SETUP_FILE "$sep(\"$1\", \"$2\")"; $sep = ", "; } + elsif (m/\s*(.*)\s*/) { + print SETUP_FILE "$sep(\"$1\", \"\")"; + $sep = ", "; + } } print SETUP_FILE "] *}\n"; }