# HG changeset patch
# User wenzelm
# Date 1625218173 -7200
# Node ID c6631069357bfcdef613069142a4a94c50fc4f12
# Parent  1f532f2b2f608c7b88a2d891f09694b83f5505ec
tuned signature;

diff -r 1f532f2b2f60 -r c6631069357b src/Tools/Setup/isabelle/setup/Build_Scala.java
--- a/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 11:23:55 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 11:29:33 2021 +0200
@@ -79,14 +79,14 @@
             return props.getProperty("main", "");
         }
 
-        public List<String> sources()
+        public String[] sources()
         {
-            return Arrays.asList(props.getProperty("sources", "").split("\\s+"));
+            return props.getProperty("sources", "").split("\\s+");
         }
 
-        public List<String> services()
+        public String[] services()
         {
-            return Arrays.asList(props.getProperty("services", "").split("\\s+"));
+            return props.getProperty("services", "").split("\\s+");
         }
 
         public Path path(String file)
@@ -118,9 +118,9 @@
         String jar_name = context.jar_name();
         String shasum_name = context.shasum_name();
 
-        List<String> sources = context.sources();
+        String[] sources = context.sources();
 
-        if (sources.isEmpty()) {
+        if (sources.length == 0) {
             Files.deleteIfExists(context.path(jar_name));
             Files.deleteIfExists(context.path(shasum_name));
         }