tuned signature;
authorwenzelm
Fri, 02 Jul 2021 11:29:33 +0200
changeset 73916 c6631069357b
parent 73915 1f532f2b2f60
child 73917 b5d52a4d6fd9
tuned signature;
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));
         }