src/Pure/Tools/build.scala
changeset 68148 fb661e4c4717
parent 68092 888d35a19866
child 68198 6710167e17af
     1.1 --- a/src/Pure/Tools/build.scala	Fri May 11 19:27:00 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri May 11 19:57:49 2018 +0200
     1.3 @@ -286,9 +286,13 @@
     1.4                  case None =>
     1.5                    for {
     1.6                      text <- Library.try_unprefix("\fexport = ", line)
     1.7 -                    (args, body) <-
     1.8 +                    (args, path) <-
     1.9                        Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
    1.10 -                  } { export_consumer(name, args, body) }
    1.11 +                  } {
    1.12 +                    val body = Bytes.read(path)
    1.13 +                    path.file.delete
    1.14 +                    export_consumer(name, args, body)
    1.15 +                  }
    1.16                },
    1.17              progress_limit =
    1.18                options.int("process_output_limit") match {