diff options
| author | Pierre-Marie Pédrot | 2018-07-26 17:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 17:56:27 +0200 |
| commit | 6eba9ffea648aace40261aa6abb5f138cad27d2d (patch) | |
| tree | dee747082b108195b266cd3b47b3299d075f8cea /plugins/syntax/plugin_base.dune | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
Fix Search query in CoqIDE.
For some reason the code was just doing random stuff that did not make
sense.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions