# HG changeset patch
# User wenzelm
# Date 1361618898 -3600
# Node ID d55cce4d72dde408494bd7fca086e1e67ec113b1
# Parent  ca13a14cc52e346191c051aaa1f34b98b00836cb
more permissive File.read_lines, which is relevant for Managed_Process join/kill;

diff -r ca13a14cc52e -r d55cce4d72dd src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Feb 23 11:27:45 2013 +0100
+++ b/src/Pure/General/file.scala	Sat Feb 23 12:28:18 2013 +0100
@@ -9,7 +9,7 @@
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader,
-  File => JFile}
+  File => JFile, IOException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 
 import scala.collection.mutable
@@ -81,7 +81,7 @@
   {
     val result = new mutable.ListBuffer[String]
     var line: String = null
-    while ({ line = reader.readLine; line != null }) {
+    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
       progress(line)
       result += line
     }