diff options
| author | Lysxia | 2019-07-27 00:15:55 -0400 |
|---|---|---|
| committer | Lysxia | 2019-07-27 00:17:30 -0400 |
| commit | c00e1184f361c506bb69f659711a0f251cc35471 (patch) | |
| tree | 7bda524067437c56b40febe91a081f6e2bb656a9 /plugins/syntax/plugin_base.dune | |
| parent | 2e37b4b30d0779dc960db80189e51ecd69f7e45a (diff) | |
[coqdoc] Simplify regex for identifiers in comments
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions