diff options
| author | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
| commit | a257ddce0ef35b8596e71377e9a1967baefebea4 (patch) | |
| tree | 0a7865ccdd9e18eceefa6e3773af51e152f4005f /doc | |
| parent | e8dbb311c82acb5cdf6d2f81dd6a1df503a7a123 (diff) | |
| parent | 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 (diff) | |
Merge PR #8182: Handle diffs better for the "Undo" command.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions