# HG changeset patch
# User egahlin
# Date 1565978410 -7200
# Node ID d8a436dfa0417a52323980b17dc0a7f706fde80e
# Parent  8173090d2794cc036d7849202606d033e7c525e4
Minor docs fix

diff -r 8173090d2794 -r d8a436dfa041 src/jdk.jfr/share/classes/jdk/jfr/consumer/EventStream.java
--- a/src/jdk.jfr/share/classes/jdk/jfr/consumer/EventStream.java	Thu Aug 15 03:00:02 2019 +0200
+++ b/src/jdk.jfr/share/classes/jdk/jfr/consumer/EventStream.java	Fri Aug 16 20:00:10 2019 +0200
@@ -203,7 +203,7 @@
      * <p>
      * The end time must be set before the stream is started.
      * <p>
-     * When the end time is reached the stream is terminated.
+     * When the end time is reached the stream is closed.
      *
      * @param endTime the end time, not {@code null}
      *
@@ -211,7 +211,6 @@
      */
     public void setEndTime(Instant endTime);
 
-
     /**
      * Start processing events in the stream.
      * <p>