# HG changeset patch
# User wenzelm
# Date 1364138394 -3600
# Node ID 9e91959a8cfcf4961d8ee4ea1be40b45c4a33320
# Parent  18095684c5a6f52997342c0ca69d69a4a1259509
prefer preset = 3 -- much faster and less memory requirement;

diff -r 18095684c5a6 -r 9e91959a8cfc src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Mar 24 16:12:45 2013 +0100
+++ b/src/Pure/General/file.scala	Sun Mar 24 16:19:54 2013 +0100
@@ -137,14 +137,12 @@
       new XZOutputStream(new BufferedOutputStream(s), options))
   }
 
-  def write_xz(file: JFile, text: CharSequence): Unit =
-    write_xz(file, text, LZMA2Options.PRESET_DEFAULT)
+  def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, 3)
 
   def write_xz(path: Path, text: CharSequence, preset: Int): Unit =
     write_xz(path.file, text, preset)
 
-  def write_xz(path: Path, text: CharSequence): Unit =
-    write_xz(path.file, text, LZMA2Options.PRESET_DEFAULT)
+  def write_xz(path: Path, text: CharSequence): Unit = write_xz(path.file, text, 3)
 
 
   /* copy */