diff options
| author | Jason Gross | 2018-11-28 15:02:56 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:02:56 -0500 |
| commit | 5537151575195addd3e1e0003025384a85d957f7 (patch) | |
| tree | 385615950292834ebcde378a51b5bfe03342c225 /plugins/syntax/plugin_base.dune | |
| parent | bc6affea2270b1182181c42f3c3f06360bf216e6 (diff) | |
Fix string notation doc
As per https://github.com/coq/coq/pull/8965/files#r237225852
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions