tuned signature;
authorwenzelm
Thu, 04 Oct 2012 11:07:36 +0200
changeset 49696 3003c87f7814
parent 49695 8f61d1c7dded
child 49697 ad2bd4e5a029
tuned signature;
src/Pure/General/sha1.scala
src/Pure/System/build.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")
--- 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 " +