# HG changeset patch
# User wenzelm
# Date 1626029275 -7200
# Node ID c9771e1b3223ea4f9dd1d3d448ae1030493d2f73
# Parent  59b6f046208609e46f70d56af8480dc0f8b72604
strict shasum: this is used on input files;

diff -r 59b6f0462086 -r c9771e1b3223 src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 16:57:30 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 20:47:55 2021 +0200
@@ -165,7 +165,11 @@
         public String shasum(String file)
             throws IOException, NoSuchAlgorithmException, InterruptedException
         {
-            return shasum(file, List.of(path(file)));
+            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()));
+            }
         }
     }