GraphicsRadioInt is used by the panes in the Graphics config window to
create radio buttons that change their associated config setting, and
update their own state when something else changes the config setting.
Despite its current name nothing about this class is particular to the
Graphics window, so renaming it to ConfigRadioInt better reflects its
purpose. This should also make it less confusing when ConfigRadioInts
are added to other config panes.
a7abd7dba0