src/Pure/Tools/build.ML
changeset 59058 a78612c67ec0
parent 58928 23d0ffd48006
child 59149 0070053570c4
     1.1 --- a/src/Pure/Tools/build.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4            (Options.bool options "document_graph")
     1.5            (Options.string options "document_output")
     1.6            (Present.document_variants (Options.string options "document_variants"))
     1.7 -          (map (pairself Path.explode) document_files)
     1.8 +          (map (apply2 Path.explode) document_files)
     1.9            parent_name (chapter, name)
    1.10            verbose;
    1.11