# HG changeset patch
# User wenzelm
# Date 1525727302 -7200
# Node ID 2277fe496d787f9fc4ba82b5e7e4be3f901fd07c
# Parent  3687109009c4ebe6d711c7cb6539abb7e69724c7
more operations;

diff -r 3687109009c4 -r 2277fe496d78 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon May 07 22:48:24 2018 +0200
+++ b/src/Pure/General/bytes.scala	Mon May 07 23:08:22 2018 +0200
@@ -56,6 +56,12 @@
     new Bytes(a, 0, n)
   }
 
+  def base64(s: String): Bytes =
+  {
+    val a = Base64.getDecoder.decode(s)
+    new Bytes(a, 0, a.length)
+  }
+
 
   /* read */