src/Pure/Tools/build.ML
changeset 56530 5c178501cf78
parent 55448 e42a3fc18458
child 56533 cd8b6d849b6a
     1.1 --- a/src/Pure/Tools/build.ML	Thu Apr 10 15:14:38 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Thu Apr 10 18:13:44 2014 +0200
     1.3 @@ -157,7 +157,6 @@
     1.4            (Options.string options "document_output")
     1.5            document_variants
     1.6            parent_name (chapter, name)
     1.7 -          (false, "")
     1.8            verbose;
     1.9  
    1.10        val last_timing = lookup_timings (fold update_timings command_timings empty_timings);