# HG changeset patch
# User wenzelm
# Date 1475490262 -7200
# Node ID 73af1d36aeff853166cd8fd8fc7aa739e0f3e576
# Parent  08f89f0e8a62772c2b1d344f38067b05fc6d724d
tuned signature;

diff -r 08f89f0e8a62 -r 73af1d36aeff src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Oct 03 10:51:51 2016 +0200
+++ b/src/Pure/General/file.scala	Mon Oct 03 12:24:22 2016 +0200
@@ -227,7 +227,7 @@
     try { writer.append(text) } finally { writer.close }
   }
 
-  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, (s) => s)
+  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
 
   def write_gzip(file: JFile, text: CharSequence): Unit =
@@ -235,9 +235,11 @@
   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
 
   def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
-    File.write_file(file, text, (s) => new XZOutputStream(new BufferedOutputStream(s), options))
+    File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
+  def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
   def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
     write_xz(path.file, text, options)
+  def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
 
   def write_backup(path: Path, text: CharSequence)
   {