src/Pure/Tools/build.ML

--- a/src/Pure/Tools/build.ML	Mon Mar 11 13:28:46 2013 +0100
+++ b/src/Pure/Tools/build.ML	Mon Mar 11 14:25:14 2013 +0100
@@ -136,7 +136,7 @@
           (Options.string options "document_output")
           document_variants
           parent_name name
-          (false, "") ""
+          (false, "")
           verbose;
 
       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);