src/HOL/Mirabelle/lib/scripts/mirabelle.pl
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";
   }