src/Pure/System/platform.scala
changeset 73439 b8e12e94cfca
parent 72603 e25c0a6cc335
child 73858 37243ad3ecb6
equal deleted inserted replaced
73438:e7437085e589 73439:b8e12e94cfca
    30       catch { case _: NoSuchElementException => None }
    30       catch { case _: NoSuchElementException => None }
    31 
    31 
    32     def parse(name: String): Value =
    32     def parse(name: String): Value =
    33       unapply(name) getOrElse error("Bad platform family: " + quote(name))
    33       unapply(name) getOrElse error("Bad platform family: " + quote(name))
    34   }
    34   }
       
    35 
       
    36   def standard_platform(platform: Family.Value): String =
       
    37     platform match {
       
    38       case Platform.Family.linux => "x86_64-linux"
       
    39       case Platform.Family.macos => "x86_64-darwin"
       
    40       case Platform.Family.windows => "x86_64-cygwin"
       
    41     }
    35 
    42 
    36 
    43 
    37   /* platform identifiers */
    44   /* platform identifiers */
    38 
    45 
    39   private val X86 = """i.86|x86""".r
    46   private val X86 = """i.86|x86""".r