# HG changeset patch
# User wenzelm
# Date 1458822122 -3600
# Node ID 01b71da798ddd78850a13e5893c8810ea80daef6
# Parent  e29f47e04180c22c924fe68786cf400be523976f
more operations;

diff -r e29f47e04180 -r 01b71da798dd src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Mar 24 13:08:12 2016 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 24 13:22:02 2016 +0100
@@ -10,7 +10,8 @@
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
+  Files, SimpleFileVisitor, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, URLDecoder, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
@@ -238,6 +239,15 @@
   }
 
 
+  /* append */
+
+  def append(file: JFile, text: CharSequence): Unit =
+    Files.write(file.toPath, UTF8.bytes(text.toString),
+      StandardOpenOption.APPEND, StandardOpenOption.CREATE)
+
+  def append(path: Path, text: CharSequence): Unit = append(path.file, text)
+
+
   /* copy */
 
   def eq(file1: JFile, file2: JFile): Boolean =