| changeset 50203 | 00d8ad713e32 |
| parent 49696 | 3003c87f7814 |
| child 54440 | 2c4940d2edf7 |
--- a/src/Pure/General/sha1.scala Sun Nov 25 19:55:42 2012 +0100 +++ b/src/Pure/General/sha1.scala Sun Nov 25 20:17:04 2012 +0100 @@ -56,6 +56,6 @@ make_result(digest) } - def digest(string: String): Digest = digest(Standard_System.string_bytes(string)) + def digest(string: String): Digest = digest(UTF8.string_bytes(string)) }