# HG changeset patch
# User wenzelm
# Date 1285536910 -7200
# Node ID 6e74fb2d4374257ad173021823919858ac27d95a
# Parent  41e9f69c553df6d8ede671a6a4fdfa01afd1d325
raw_untar.raw_execute with native cwd, to avoid cross-platform complications;
more informative treatment of IOException, notably due to broken pipe;

diff -r 41e9f69c553d -r 6e74fb2d4374 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