--- a/langtools/src/jdk.jshell/share/classes/jdk/jshell/execution/PipeInputStream.java	Wed Jul 05 22:21:06 2017 +0200
+++ b/langtools/src/jdk.jshell/share/classes/jdk/jshell/execution/PipeInputStream.java	Tue Oct 18 16:00:32 2016 +0200
@@ -42,7 +42,7 @@
 
     @Override
     public synchronized int read() throws IOException {
-        if (start == end) {
+        if (start == end && !closed) {
             inputNeeded();
         }
         while (start == end) {
@@ -62,6 +62,32 @@
         }
     }
 
+    @Override
+    public synchronized int read(byte[] b, int off, int len) throws IOException {
+        if (b == null) {
+            throw new NullPointerException();
+        } else if (off < 0 || len < 0 || len > b.length - off) {
+            throw new IndexOutOfBoundsException();
+        } else if (len == 0) {
+            return 0;
+        }
+
+        int c = read();
+        if (c == -1) {
+            return -1;
+        }
+        b[off] = (byte)c;
+
+        int totalRead = 1;
+        while (totalRead < len && start != end) {
+            int r = read();
+            if (r == (-1))
+                break;
+            b[off + totalRead++] = (byte) r;
+        }
+        return totalRead;
+    }
+
     protected void inputNeeded() throws IOException {}
 
     private synchronized void write(int b) {