diff options
| author | Gaëtan Gilbert | 2019-02-14 15:12:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:10 +0100 |
| commit | 7cb49eda2c33c620f020cf7487ab9f53b74859da (patch) | |
| tree | 6680f9380932fd53e3198518aa28063871fe4835 /plugins/syntax/plugin_base.dune | |
| parent | eb20b899a6cd0e3b9816a4b6824998255c4af6b8 (diff) | |
Sphinx: remove [coqtop:: undo]
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions