--- a/src/Pure/General/sha1.scala Thu Oct 04 10:55:36 2012 +0200
+++ b/src/Pure/General/sha1.scala Thu Oct 04 11:07:36 2012 +0200
@@ -48,8 +48,6 @@
make_result(digest)
}
- def digest(path: Path): Digest = digest(path.file)
-
def digest(bytes: Array[Byte]): Digest =
{
val digest = MessageDigest.getInstance("SHA")
--- a/src/Pure/System/build.scala Thu Oct 04 10:55:36 2012 +0200
+++ b/src/Pure/System/build.scala Thu Oct 04 11:07:36 2012 +0200
@@ -374,7 +374,7 @@
echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
val sources =
- try { all_files.map(p => (p, SHA1.digest(p))) }
+ try { all_files.map(p => (p, SHA1.digest(p.file))) }
catch {
case ERROR(msg) =>
error(msg + "\nThe error(s) above occurred in session " +