changeset 80365 | 29b761e290c5 |
parent 80194 | 79655411a32d |
child 80378 | ab4badc7db7f |
--- a/src/Pure/General/file.scala Thu Jun 13 15:08:24 2024 +0200 +++ b/src/Pure/General/file.scala Sat Jun 15 12:27:57 2024 +0200 @@ -355,7 +355,7 @@ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false - else Bytes.read(file1) == Bytes.read(file2) + else SHA1.digest(file1) == SHA1.digest(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)