If we modify an option that may have been specified by users, we may
make unintended changes, so it is better not to modify it as much as
possible, IMO.