# HG changeset patch
# User wenzelm
# Date 1718447277 -7200
# Node ID 29b761e290c556512d829a84f8a063f72f2f8ab6
# Parent  d5c48fe601b63303821068be440259db9810f74a
clarified File.eq_content, following 306f273c91ec;

diff -r d5c48fe601b6 -r 29b761e290c5 src/Pure/General/file.scala
--- 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)