| changeset 69754 | 8d548b8f63ca |
| parent 69425 | 94f6ca69d983 |
| child 71601 | 97ccf48c2f0c |
--- a/src/Pure/Admin/build_jdk.scala Tue Jan 29 21:56:40 2019 +0100 +++ b/src/Pure/Admin/build_jdk.scala Tue Jan 29 22:47:45 2019 +0100 @@ -20,7 +20,7 @@ def detect_version(s: String): String = { - val Version_Dir_Entry = """^jdk-(\d+\+\d+)$""".r + val Version_Dir_Entry = """^jdk-([0-9.]+\+\d+)$""".r s match { case Version_Dir_Entry(version) => version case _ => error("Cannot detect JDK version from " + quote(s))