Changing diff options is implemented by modifying the session data and using a ''redirect''. Therefore, one must be sure that the changes to the session are saved ''before'' a new session object for the redirected request gets created.
Authored by: cboos 2005-06-14
Parent: [r1786]
Child: [r1788]
