src/Pure/Tools/build.scala
changeset 65517 1544e61e5314
parent 65506 359fc6266a00
child 65520 f47bc12b6e8a
--- a/src/Pure/Tools/build.scala	Wed Apr 19 16:26:09 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 19 20:10:34 2017 +0200
@@ -203,7 +203,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                pair(list(pair(Options.encode, list(string))),
+                pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, string)), pair(list(pair(string, string)),
                 list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,