# HG changeset patch # User wenzelm # Date 1656422957 -7200 # Node ID 809c37bfd8234198511ef34f55b9c92b7f743859 # Parent e3aa7214eb1ab6eaa0a2d86028a3caef78d9943d clarified IO, following Java 11 and Isabelle/Scala; diff -r e3aa7214eb1a -r 809c37bfd823 src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Tue Jun 28 15:23:05 2022 +0200 +++ b/src/Pure/Admin/ci_profile.scala Tue Jun 28 15:29:17 2022 +0200 @@ -10,6 +10,7 @@ import java.time.{Instant, ZoneId} import java.time.format.DateTimeFormatter import java.util.{Properties => JProperties, Map => JMap} +import java.nio.file.Files object CI_Profile { @@ -78,15 +79,13 @@ private def load_properties(): JProperties = { - val props = new JProperties() + val props = new JProperties val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") - - if (file_name != "") { - val file = Path.explode(file_name).file - if (file.exists()) props.load(new java.io.FileReader(file)) - props + if (file_name.nonEmpty) { + val path = Path.explode(file_name) + if (path.is_file) props.load(Files.newBufferedReader(path.java_path)) } - else props + props } private def compute_timing(results: Build.Results, group: Option[String]): Timing = {