author | wenzelm |
Sun, 03 Jan 2021 12:11:56 +0100 | |
changeset 73035 | 03e78b35ebbc |
parent 73034 | 43c534bba442 |
child 73036 | b028e8d22d8d |
--- a/src/Pure/Tools/scala_project.scala Sat Jan 02 23:03:47 2021 +0100 +++ b/src/Pure/Tools/scala_project.scala Sun Jan 03 12:11:56 2021 +0100 @@ -38,6 +38,7 @@ List( Path.explode("~~/lib/classes/Pure.shasum"), Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum")) + if path.is_file line <- Library.trim_split_lines(File.read(path)) name = if (line.length > 42 && line(41) == '*') line.substring(42)