raw_untar.raw_execute with native cwd, to avoid cross-platform complications;
authorwenzelm
Sun, 26 Sep 2010 23:35:10 +0200
changeset 39706 6e74fb2d4374
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
--- a/src/Pure/System/standard_system.scala	Sun Sep 26 22:54:37 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Sun Sep 26 23:35:10 2010 +0200
@@ -189,18 +189,20 @@
     }
     val gzip_stream = new GZIPInputStream(progress_stream)
 
-    val proc = raw_execute(null, null, false, tar, "-C", root.getCanonicalPath, "-x", "-f", "-")
+    val proc = raw_execute(root, null, false, tar, "-x", "-f", "-")
     val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
     val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
     val stdin = new BufferedOutputStream(proc.getOutputStream)
 
     try {
       var c = -1
-      while ({ c = gzip_stream.read; c != -1 }) stdin.write(c)
+      val io_err =
+        try { while ({ c = gzip_stream.read; c != -1 }) stdin.write(c); false }
+        catch { case e: IOException => true }
       stdin.close
 
       val rc = try { proc.waitFor } finally { Thread.interrupted }
-      if (rc != 0) error(stderr.join.trim) else stdout.join
+      if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
     }
     finally {
       gzip_stream.close