diff options
| author | Enrico Tassi | 2018-07-27 08:54:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-07-27 08:54:59 +0200 |
| commit | 9f9a7736c24270a3f3d8177c65e80a1ee04c4615 (patch) | |
| tree | 38063548ea66c1c78c4294612f0cf15d2350fa33 /plugins/syntax/string_syntax_plugin.mlpack | |
| parent | 06c78339555a47cebc0f2c0ce4daa6c97488024d (diff) | |
| parent | 6625887dc2a5c67f7cb93435795129af2cfabb84 (diff) | |
Merge PR #8141: Diff option in CoqIDE
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions