src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Sun Apr 13 16:06:55 2014 +0200
+++ b/src/Pure/System/options.scala	Sun Apr 13 16:42:44 2014 +0200
@@ -50,7 +50,7 @@
     def print: String = print(false)
     def print_default: String = print(true)
 
-    def title(strip: String): String =
+    def title(strip: String = ""): String =
     {
       val words = space_explode('_', name)
       val words1 =