MediaWiki needs a maintenance scripts to cleanup the user_properties table.

bug 28343 removes preferences and the new script should remove the rows from users which have set the preference.

You can design the script in two ways:

1. Removing a named preference from the table, useful when adding a preference to $wgHiddenPrefs
2. Check for all current preferences be set. Useful to run after a upgrade or so (ConvertUserOptions looks to expensive for that).

Thanks.

Version: 1.20.x
Severity: enhancement