Commit 85e8bea4fdecc841b1ea6303ab7ca09813b3869b

Werner Lemberg 2018-07-31T10:42:21

Minor documentation improvement.