src/Pure/Tools/build_console.scala
changeset 57581 74bbe9317aa4
parent 57580 86b413b8f779
child 60518 a79f89a36dff
     1.1 --- a/src/Pure/Tools/build_console.scala	Sun Jul 20 17:21:14 2014 +0200
     1.2 +++ b/src/Pure/Tools/build_console.scala	Sun Jul 20 17:54:01 2014 +0200
     1.3 @@ -40,8 +40,11 @@
     1.4            session ::
     1.5            Properties.Value.Boolean(no_build) ::
     1.6            Properties.Value.Boolean(system_mode) ::
     1.7 -          Command_Line.Chunks(dirs, build_options) =>
     1.8 -            val options = (Options.init() /: build_options)(_ + _)
     1.9 +          options_file ::
    1.10 +          Command_Line.Chunks(dirs, system_options) =>
    1.11 +            val options = (Options.init() /: system_options)(_ + _)
    1.12 +            File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
    1.13 +
    1.14              val progress = new Build.Console_Progress()
    1.15              progress.interrupt_handler {
    1.16                build_console(options, progress,