diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 18:27:20 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 18:27:20 +0100 |
| commit | f0cb72dded093175feab3f19aac63fab46999e0a (patch) | |
| tree | 52d16e09ce2b65cbdd56ad6a542b04c01438b77a /dev/base_include | |
| parent | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (diff) | |
[dune] [ide] Install data files.
We should install the files in `share/coqide` instead of the current
`coq` location; but we defer this change until we are more advanced in
the make-phase out.
Fixes: #8953
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions