# 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 = {