src/Pure/System/build.scala
changeset 48344 8dc904c45945
parent 48341 752de4e10162
child 48346 e2382bede914
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 20:59:02 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 11:47:49 2012 +0200
     1.3 @@ -162,16 +162,6 @@
     1.4  
     1.5    /** command line entry point **/
     1.6  
     1.7 -  private object Bool
     1.8 -  {
     1.9 -    def unapply(s: String): Option[Boolean] =
    1.10 -      s match {
    1.11 -        case "true" => Some(true)
    1.12 -        case "false" => Some(false)
    1.13 -        case _ => None
    1.14 -      }
    1.15 -  }
    1.16 -
    1.17    private object Chunks
    1.18    {
    1.19      private def chunks(list: List[String]): List[List[String]] =
    1.20 @@ -189,7 +179,10 @@
    1.21      val rc =
    1.22        try {
    1.23          args.toList match {
    1.24 -          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
    1.25 +          case
    1.26 +            Properties.Value.Boolean(all_sessions) ::
    1.27 +            Properties.Value.Boolean(build_images) ::
    1.28 +            Properties.Value.Boolean(list_only) ::
    1.29              Chunks(more_dirs, options, sessions) =>
    1.30                build(all_sessions, build_images, list_only,
    1.31                  more_dirs.map(Path.explode), options, sessions)