# HG changeset patch
# User wenzelm
# Date 1625217835 -7200
# Node ID 1f532f2b2f608c7b88a2d891f09694b83f5505ec
# Parent  4be1047576e64fb51cc87659525b2ec0a7936e39
tuned;

diff -r 4be1047576e6 -r 1f532f2b2f60 src/Tools/Setup/isabelle/setup/Build_Scala.java
--- a/src/Tools/Setup/isabelle/setup/Build_Scala.java	Thu Jul 01 23:27:43 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 11:23:55 2021 +0200
@@ -64,6 +64,16 @@
             return props.getProperty("lib", "lib") + "/" + name();
         }
 
+        public String jar_name()
+        {
+            return lib_name() + ".jar";
+        }
+
+        public String shasum_name()
+        {
+            return lib_name() + ".shasum";
+        }
+
         public String main()
         {
             return props.getProperty("main", "");
@@ -105,8 +115,8 @@
     public static void build_scala(Context context, boolean fresh)
         throws IOException, InterruptedException, NoSuchAlgorithmException
     {
-        String jar_name = context.lib_name() + ".jar";
-        String shasum_name = context.lib_name() + ".shasum";
+        String jar_name = context.jar_name();
+        String shasum_name = context.shasum_name();
 
         List<String> sources = context.sources();