src/Pure/Tools/build.scala
changeset 65392 f365f61f2081
parent 65374 a5b38d8d3c1e
child 65406 cc9e2f1f279d
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 05 11:39:36 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 05 22:00:44 2017 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
     1.5                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     1.6                  pair(string, pair(string, pair(string, pair(Path.encode,
     1.7 -                list(pair(Options.encode, list(Path.encode))))))))))))))(
     1.8 +                list(pair(Options.encode, list(string))))))))))))))(
     1.9                (Symbol.codes, (command_timings, (do_output, (verbose,
    1.10                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    1.11                  (parent, (info.chapter, (name, (Path.current,