src/Pure/Tools/build.scala
changeset 67493 c4e9e0c50487
parent 67471 bddfa23a4ea9
child 67782 7e223a05e6d8
     1.1 --- a/src/Pure/Tools/build.scala	Tue Jan 23 17:58:09 2018 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Jan 23 19:25:39 2018 +0100
     1.3 @@ -212,7 +212,8 @@
     1.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     1.5                  pair(string, pair(string, pair(string, pair(Path.encode,
     1.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
     1.7 -                pair(list(string), pair(list(string), pair(list(pair(string, string)),
     1.8 +                pair(list(pair(string, properties)), pair(list(string),
     1.9 +                pair(list(pair(string, string)),
    1.10                  pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
    1.11                (Symbol.codes, (command_timings, (do_output, (verbose,
    1.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),