# 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)