diff options
| author | Jim Fehrle | 2018-08-14 21:37:12 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-08-16 23:19:15 -0700 |
| commit | 99c9fb61fd702693807f0558b04e5134e08e87bb (patch) | |
| tree | 5cd2dcedb70c43769deaa761355da2ff65f2ec47 /dev/ci/ci-basic-overlay.sh | |
| parent | 8b176e3b0e42b34db3165d9e1ce45fff0e581335 (diff) | |
1) Make the diff setting a persistent settting.
2) Changing the diff setting from the menu should reprint the proof.
3) Generate a warning message if the user enters a "Set Diffs xx" command.
4) Tweak display names for diffs in View menu.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions