src/Pure/Admin/build_polyml.scala
changeset 72351 68902f8a1ef0
parent 71726 a5fda30edae2
child 72352 f4bd6f123fdf
equal deleted inserted replaced
72350:95c2853dd616 72351:68902f8a1ef0
    62 
    62 
    63     val platform = platform_arch + "-" + platform_os
    63     val platform = platform_arch + "-" + platform_os
    64     val platform_64 = "x86_64-" + platform_os
    64     val platform_64 = "x86_64-" + platform_os
    65 
    65 
    66     val info =
    66     val info =
    67       platform_info.get(platform_os) getOrElse
    67       platform_info.getOrElse(platform_os,
    68         error("Bad OS platform: " + quote(platform_os))
    68         error("Bad OS platform: " + quote(platform_os)))
    69 
    69 
    70     val settings =
    70     val settings =
    71       msys_root match {
    71       msys_root match {
    72         case None if Platform.is_windows =>
    72         case None if Platform.is_windows =>
    73           error("Windows requires specification of msys root directory")
    73           error("Windows requires specification of msys root directory")