--- a/src/Pure/System/platform.scala Wed Mar 27 15:38:41 2024 +0100
+++ b/src/Pure/System/platform.scala Wed Mar 27 17:04:37 2024 +0100
@@ -81,6 +81,17 @@
/* platform info */
+ object Info {
+ def check(infos: List[Info], spec: String): String = {
+ val specs = Library.distinct(infos.map(_.family_name) ::: infos.map(_.platform))
+ if (specs.contains(spec)) spec
+ else {
+ error("Bad platform specification " + quote(spec) +
+ "\n expected " + commas_quote(specs))
+ }
+ }
+ }
+
trait Info {
def platform: String
override def toString: String = platform
@@ -97,15 +108,6 @@
def is(spec: String): Boolean = platform == spec || family_name == spec
}
- def check_spec(infos: List[Info], spec: String): String = {
- val specs = Library.distinct(infos.map(_.family_name) ::: infos.map(_.platform))
- if (specs.contains(spec)) spec
- else {
- error("Bad platform specification " + quote(spec) +
- "\n expected " + commas_quote(specs))
- }
- }
-
/* JVM version */