# HG changeset patch
# User wenzelm
# Date 1626030791 -7200
# Node ID 472bdccfba6203deec59f18d93f8413cdb9c705e
# Parent  f6862d5f4e7fca1a1bedd5de2f93fd1b39bd63d7
even more strict shasum (amending c9771e1b3223);

diff -r f6862d5f4e7f -r 472bdccfba62 src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 21:00:41 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 21:13:11 2021 +0200
@@ -152,29 +152,24 @@
         public String shasum(String name, List<Path> paths)
             throws IOException, NoSuchAlgorithmException
         {
-            boolean exists = false;
             MessageDigest sha = MessageDigest.getInstance("SHA");
             for (Path file : paths) {
                 if (Files.exists(file)) {
-                    exists = true;
                     sha.update(Files.readAllBytes(file));
                 }
+                else {
+                    throw new RuntimeException(
+                        "Missing input file " + Environment.quote(file.toString()));
+                }
             }
-            if (exists) {
-                String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
-                return digest + " " + name + "\n";
-            }
-            else { return ""; }
+            String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
+            return digest + " " + name + "\n";
         }
 
         public String shasum(String file)
             throws IOException, NoSuchAlgorithmException, InterruptedException
         {
-            Path path = path(file);
-            if (Files.exists(path)) { return shasum(file, List.of(path)); }
-            else {
-                throw new RuntimeException("Missing input file " + Environment.quote(path.toString()));
-            }
+            return shasum(file, List.of(path(file)));
         }
     }