# HG changeset patch
# User wenzelm
# Date 1627139210 -7200
# Node ID 4b15a1e25537beea5cf784c072140deb580d7ac8
# Parent  22ad3ac2152c134465726acbab1a88037408c2d8
more robust;

diff -r 22ad3ac2152c -r 4b15a1e25537 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)