src/Pure/Tools/scala_build.scala
changeset 75687 c8dc5d1adc7b
parent 75678 58b161746645
child 75869 ee2f93fa2440
equal deleted inserted replaced
75686:42f19e398ee4 75687:c8dc5d1adc7b
    96 
    96 
    97   object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun {
    97   object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun {
    98     val here = Scala_Project.here
    98     val here = Scala_Project.here
    99     def invoke(args: List[Bytes]): List[Bytes] =
    99     def invoke(args: List[Bytes]): List[Bytes] =
   100       args match {
   100       args match {
   101         case List(component, dir) =>
   101         case List(dir) =>
   102           val result =
   102           val result = build_result(Path.explode(dir.text))
   103             build_result(Path.explode(dir.text),
       
   104               component = Value.Boolean.parse(component.text))
       
   105           val jar_name =
   103           val jar_name =
   106             result.jar_path match {
   104             result.jar_path match {
   107               case Some(path) => path.file_name
   105               case Some(path) => path.file_name
   108               case None => "scala_build.jar"
   106               case None => "scala_build.jar"
   109             }
   107             }