--- a/src/Pure/Tools/build.scala Tue Feb 19 12:58:32 2013 +0100
+++ b/src/Pure/Tools/build.scala Tue Feb 19 13:57:13 2013 +0100
@@ -443,10 +443,10 @@
else
{
import XML.Encode._
- pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
- pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
- (do_output, (info.options, (verbose, (browser_info, (parent,
- (name, info.theories)))))))
+ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
+ pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+ (Nil /* FIXME */, (do_output, (info.options, (verbose, (browser_info,
+ (parent, (name, info.theories))))))))
}))
private val env =