Integrated: 6837: More formal tone in the agent settings

Tue Oct 6 10:59:40 UTC 2020

On Fri, 2 Oct 2020 22:28:39 GMT, Marcus Hirt <hirt at openjdk.org> wrote:

> Wasn't as bad as I remembered it.

This pull request has now been integrated.

Changeset: e74a5ff3
Author:    Marcus Hirt <hirt at openjdk.org>
URL:       https://git.openjdk.java.net/jmc/commit/e74a5ff3
Stats:     14 lines in 2 files changed: 2 ins; 0 del; 12 mod

6837: More formal tone in the agent settings

Reviewed-by: ghb

-------------

PR: https://git.openjdk.java.net/jmc/pull/118