equal
deleted
inserted
replaced
36 (for { |
36 (for { |
37 path <- |
37 path <- |
38 List( |
38 List( |
39 Path.explode("~~/lib/classes/Pure.shasum"), |
39 Path.explode("~~/lib/classes/Pure.shasum"), |
40 Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum")) |
40 Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum")) |
|
41 if path.is_file |
41 line <- Library.trim_split_lines(File.read(path)) |
42 line <- Library.trim_split_lines(File.read(path)) |
42 name = |
43 name = |
43 if (line.length > 42 && line(41) == '*') line.substring(42) |
44 if (line.length > 42 && line(41) == '*') line.substring(42) |
44 else error("Bad shasum entry: " + quote(line)) |
45 else error("Bad shasum entry: " + quote(line)) |
45 if name != "lib/classes/Pure.jar" && |
46 if name != "lib/classes/Pure.jar" && |