# HG changeset patch
# User wenzelm
# Date 1687438297 -7200
# Node ID da721ba809a4e1f8cc3f97e1f36d7a3d6c57b3ca
# Parent  443a443bbe7bb12c929e27a7f390d2bc87cec6da
more operations;

diff -r 443a443bbe7b -r da721ba809a4 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Thu Jun 22 14:29:05 2023 +0200
+++ b/src/Pure/General/bytes.scala	Thu Jun 22 14:51:37 2023 +0200
@@ -103,6 +103,14 @@
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
+
+
+  /* append */
+
+  def append(file: JFile, bytes: Bytes): Unit =
+    using(new FileOutputStream(file, true))(bytes.write_stream(_))
+
+  def append(path: Path, bytes: Bytes): Unit = append(path.file, bytes)
 }
 
 final class Bytes private(