diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2019-08-25 22:32:05 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-25 22:32:05 +0200 |
| commit | 41b5c6295278cb00b0372b01481c674561e8f4ef (patch) | |
| tree | 86e5e6ccf59933af3bd6439d51fe087424c759be /doc/Makefile | |
| parent | 6d6d4371467a94c01418e9d475e994fe61b7b4d0 (diff) | |
| parent | 32d5427f550b4c67e3dbc2bd157b83612787534b (diff) | |
Merge pull request #31654 from Paulb23/minimap_fixes
Viewport highlight, colour cache and minimap scrolling fixes.
Diffstat (limited to 'doc/Makefile')
0 files changed, 0 insertions, 0 deletions