more robust;
authorwenzelm
Sat, 24 Jul 2021 17:06:50 +0200
changeset 74058 4b15a1e25537
parent 74057 22ad3ac2152c
child 74059 55505e7bbfb3
more robust;
src/Tools/Setup/src/Build.java
--- a/src/Tools/Setup/src/Build.java	Sat Jul 24 16:40:10 2021 +0200
+++ b/src/Tools/Setup/src/Build.java	Sat Jul 24 17:06:50 2021 +0200
@@ -329,9 +329,8 @@
     private static String SHASUM = "META-INF/isabelle/shasum";
 
     public static String get_shasum(Path jar_path)
-        throws IOException
     {
-        if (Files.exists(jar_path)) {
+        try {
             try (JarFile jar_file = new JarFile(jar_path.toFile()))
             {
                 JarEntry entry = jar_file.getJarEntry(SHASUM);
@@ -342,7 +341,7 @@
                 else { return ""; }
             }
         }
-        else { return ""; }
+        catch (IOException exn) { return ""; }
     }
 
     public static void create_shasum(Path dir, String shasum)