Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Simplify away the useless option, as documented: "An option handled by your GUI. This currently doesn't do anything." The option was originally added with the introduction of contempt (e9aeaad), but it is now no longer used. closes #4918 No functional change
- Loading branch information