prefer preset = 3 -- much faster and less memory requirement;
authorwenzelm
Sun, 24 Mar 2013 16:19:54 +0100
changeset 51505 9e91959a8cfc
parent 51504 18095684c5a6
child 51506 cd573f1a82b2
child 51507 ebd5366e7a42
prefer preset = 3 -- much faster and less memory requirement;
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 */