src/Pure/Tools/build.scala
changeset 67847 c61acb4855b6
parent 67846 bdf6933f7ac9
child 67852 f701a1d5d852
     1.1 --- a/src/Pure/Tools/build.scala	Tue Mar 13 18:28:12 2018 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 13 18:40:25 2018 +0100
     1.3 @@ -699,7 +699,7 @@
     1.4      var check_keywords: Set[String] = Set.empty
     1.5      var list_files = false
     1.6      var no_build = false
     1.7 -    var options = (Options.init() /: build_options)(_ + _)
     1.8 +    var options = Options.init(opts = build_options)
     1.9      var system_mode = false
    1.10      var verbose = false
    1.11      var exclude_sessions: List[String] = Nil