# HG changeset patch
# User wenzelm
# Date 1349341656 -7200
# Node ID 3003c87f78144522403e3634be90b87693b58d80
# Parent  8f61d1c7ddedb4798cd313772cd43f9ae8e03a58
tuned signature;

diff -r 8f61d1c7dded -r 3003c87f7814 src/Pure/General/sha1.scala
--- 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")
diff -r 8f61d1c7dded -r 3003c87f7814 src/Pure/System/build.scala
--- 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 " +