src/Pure/System/build.scala
changeset 48368 dc538eef2cf2
parent 48364 9091b659d7b6
child 48370 d0fa3efec93b
     1.1 --- a/src/Pure/System/build.scala	Fri Jul 20 16:47:17 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 16:47:43 2012 +0200
     1.3 @@ -257,6 +257,8 @@
     1.4    {
     1.5      val full_queue = find_sessions(more_dirs)
     1.6  
     1.7 +    val build_options = (Options.init() /: options)(_.define_simple(_))
     1.8 +
     1.9      sessions.filter(name => !full_queue.defined(name)) match {
    1.10        case Nil =>
    1.11        case bad => error("Undefined session(s): " + commas_quote(bad))