6f9b9b6671
OLD_OPT = NEW_OPT in options* files will now map OLD_OPT to NEW_OPT with a friendly message. This is indented for situations where we need to preserve an interface in the config file in an upwards compatible fashion on a stable branch. Reviewed by: nwhitehorn@ MFC after: 3 days