I can confirm that the board discussed this proposal and their was only support for making the change in question.

Renaming of global groups is done via the on-wiki interface, and does not require a system change. Suggest closing as invalid

In T256299#6254960, @DannyS712 wrote:

Renaming of global groups is done via the on-wiki interface, and does not require a system change. Suggest closing as invalid

Message keys and values need renaming in WikimediaMessages

	"group-ombudsman": "Ombudsmen",
	"group-ombudsman-member": "{{GENDER:$1|ombudsman}}",
	"grouppage-ombudsman": "m:Ombudsman commission",

In T256299#6254960, @DannyS712 wrote:

Renaming of global groups is done via the on-wiki interface, and does not require a system change. Suggest closing as invalid

Phabricator use is encouraged for other types of Wikimedia project beyond software changes, such as Comms initiatives. Coordinating this change that might only be an email list name change and a wiki interface config is still part of how we want Phabricator to be of value and helps serve as a record of what was changed and can be quoted in other minor changes to avoid accidental systemic bias.

Change 608210 had a related patch set uploaded (by Majavah; owner: Majavah):
[mediawiki/extensions/WikimediaMessages@master] Add messages for "ombuds" group

https://gerrit.wikimedia.org/r/c/mediawiki/extensions/WikimediaMessages/ /608210

In T256299#6262399, @Majavah wrote:

Feel free to correct me if I'm wrong, but afaik in this case we need to 1) add message keys for group-ombuds 2) wait for the new messages to go out with the train everywhere 3) rename the group on-wiki and 4) after that we can remove old message keys for group-ombudsmen (which should not be renamed as the content will change)

Yup

Interestingly, some translations (ie at) have already made it gender neutral :)

	"group-ombudsman": "Ombudspersonat",

Similar for German, and some just use "mediator"

Change 608210 merged by jenkins-bot:
[mediawiki/extensions/WikimediaMessages@master] Add messages for "ombuds" group

https://gerrit.wikimedia.org/r/c/mediawiki/extensions/WikimediaMessages/ /608210

Change 609389 had a related patch set uploaded (by Majavah; owner: Majavah):
[mediawiki/extensions/WikimediaMessages@master] Remove messages for "ombudsman" global group

https://gerrit.wikimedia.org/r/609389

Change 609389 merged by jenkins-bot:
[mediawiki/extensions/WikimediaMessages@master] Remove messages for "ombudsman" global group

https://gerrit.wikimedia.org/r/609389

Change 678341 had a related patch set uploaded (by Zabe; author: Zabe):

[operations/mediawiki-config@master] Replace 'ombudsman' with 'ombuds' in wmgPrivilegedGlobalGroups

https://gerrit.wikimedia.org/r/678341

Change 678341 merged by jenkins-bot:

[operations/mediawiki-config@master] Replace 'ombudsman' with 'ombuds' in wmgPrivilegedGlobalGroups

https://gerrit.wikimedia.org/r/678341

Mentioned in SAL (#wikimedia-operations) [2021-04-12T18:04:28Z] <urbanecm@deploy1002> Synchronized wmf-config/InitialiseSettings.php: ae05f7cd53925c06d8a23cb8f667a20d79ce2cff: Replace ombudsman with ombuds in wmgPrivilegedGlobalGroups (T256299) (duration: 00m 57s)