diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 18:05:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-10 19:21:34 +0200 |
| commit | 32682ed3838cb09f16eb6b7e43b6a17a4341ddff (patch) | |
| tree | ea8923768a0806e94e8d5985d8e6f38109700420 /plugins/syntax/r_syntax_plugin.mlpack | |
| parent | 040ad198e38776bb9f398329243b2fe41434f2d5 (diff) | |
[dune] Tweaks on `tools/dune`
- `coq_tex -> `coq-tex`
- we build and intall `coqworkmgr`
- remove some redundancy
Diffstat (limited to 'plugins/syntax/r_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions