diff options
| author | Hugo Herbelin | 2019-01-25 10:30:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-25 10:40:05 +0100 |
| commit | 25014277624387ecba1befb60f1c54d68eadab01 (patch) | |
| tree | 3131cc3a70b2e4e0de610594eea45d74dd12540b /plugins/syntax/plugin_base.dune | |
| parent | 41d60ea7bf034a92e2fabee40ad435ba8363a2d6 (diff) | |
Added a line about notation bug fixes.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions