diff options
| author | Emilio Jesus Gallego Arias | 2020-06-11 16:38:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-11 16:38:48 +0200 |
| commit | 7fb7c9ede2b44bac35b08d810ec9a08358d0267b (patch) | |
| tree | 8f0e599544f33c7207b5a8f954d51a02e9c1415b /plugins/syntax | |
| parent | 149d9604c56969a067ee6d9d0d51919d96cbdc7f (diff) | |
[dune] [dbg] Fix coqide target after CoqIDE move.
Fixes #12496
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions