prefer preset = 3 -- much faster and less memory requirement;
authorwenzelm
Sun Mar 24 16:19:54 2013 +0100 (2013-03-24)
changeset 515059e91959a8cfc
parent 51504 18095684c5a6
child 51506 cd573f1a82b2
child 51507 ebd5366e7a42
prefer preset = 3 -- much faster and less memory requirement;
src/Pure/General/file.scala
     1.1 --- a/src/Pure/General/file.scala	Sun Mar 24 16:12:45 2013 +0100
     1.2 +++ b/src/Pure/General/file.scala	Sun Mar 24 16:19:54 2013 +0100
     1.3 @@ -137,14 +137,12 @@
     1.4        new XZOutputStream(new BufferedOutputStream(s), options))
     1.5    }
     1.6  
     1.7 -  def write_xz(file: JFile, text: CharSequence): Unit =
     1.8 -    write_xz(file, text, LZMA2Options.PRESET_DEFAULT)
     1.9 +  def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, 3)
    1.10  
    1.11    def write_xz(path: Path, text: CharSequence, preset: Int): Unit =
    1.12      write_xz(path.file, text, preset)
    1.13  
    1.14 -  def write_xz(path: Path, text: CharSequence): Unit =
    1.15 -    write_xz(path.file, text, LZMA2Options.PRESET_DEFAULT)
    1.16 +  def write_xz(path: Path, text: CharSequence): Unit = write_xz(path.file, text, 3)
    1.17  
    1.18  
    1.19    /* copy */