SET OPTION statement for groups [CR612762]

In the Usage section for the SET OPTION statement, the third paragraph should read as follows:

“Specifying either a user ID or the PUBLIC user ID determines whether the option is set for an individual user, a user group represented by userid, or the PUBLIC user ID (the user group to which all users are a member). If the option applies to group user ID, option settings are not inherited by members of the group. If no user group is specified, the option change is applied to the currently logged-on user ID that issued the SET OPTION statement.”