diff options
| author | Emilio Jesus Gallego Arias | 2020-02-25 15:18:28 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-25 15:18:28 -0500 |
| commit | 190a3fce86f8edd7c7bb7c6d9f8ceaa1102953a0 (patch) | |
| tree | 5e62e75ec13ce70b1abaee481b20d328f128355a /plugins/syntax/plugin_base.dune | |
| parent | 91541a2d291bc82098b6c86d52670696523fb49b (diff) | |
| parent | 60cb594b3cb7d1275a4067a3cf33c902a69682c8 (diff) | |
Merge PR #11669: Remove hard to read blue color in merge-pr
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions