raw_untar.raw_execute with native cwd, to avoid cross-platform complications;
authorwenzelm
Sun Sep 26 23:35:10 2010 +0200 (2010-09-26)
changeset 397066e74fb2d4374
parent 39705 41e9f69c553d
child 39707 4977324373f2
raw_untar.raw_execute with native cwd, to avoid cross-platform complications;
more informative treatment of IOException, notably due to broken pipe;
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/System/standard_system.scala	Sun Sep 26 22:54:37 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Sun Sep 26 23:35:10 2010 +0200
     1.3 @@ -189,18 +189,20 @@
     1.4      }
     1.5      val gzip_stream = new GZIPInputStream(progress_stream)
     1.6  
     1.7 -    val proc = raw_execute(null, null, false, tar, "-C", root.getCanonicalPath, "-x", "-f", "-")
     1.8 +    val proc = raw_execute(root, null, false, tar, "-x", "-f", "-")
     1.9      val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
    1.10      val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
    1.11      val stdin = new BufferedOutputStream(proc.getOutputStream)
    1.12  
    1.13      try {
    1.14        var c = -1
    1.15 -      while ({ c = gzip_stream.read; c != -1 }) stdin.write(c)
    1.16 +      val io_err =
    1.17 +        try { while ({ c = gzip_stream.read; c != -1 }) stdin.write(c); false }
    1.18 +        catch { case e: IOException => true }
    1.19        stdin.close
    1.20  
    1.21        val rc = try { proc.waitFor } finally { Thread.interrupted }
    1.22 -      if (rc != 0) error(stderr.join.trim) else stdout.join
    1.23 +      if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
    1.24      }
    1.25      finally {
    1.26        gzip_stream.close