diff options
| author | Théo Zimmermann | 2018-10-11 14:34:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-11 14:34:58 +0200 |
| commit | ea62cca89773e8101b7a81d15adbf15081eb5e0f (patch) | |
| tree | 201ff4ad740f8662ff2f1a852f1885367ca7085a /plugins/quote/plugin_base.dune | |
| parent | 12527ad84e9d06a124086b1d184f56eff2772b9c (diff) | |
| parent | 32682ed3838cb09f16eb6b7e43b6a17a4341ddff (diff) | |
Merge PR #8697: [dune] Fix public name of tool: coq_tex -> coq-tex
Diffstat (limited to 'plugins/quote/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions