diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 18:49:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-06 10:35:48 +0100 |
| commit | b41a051cf56a8c32b02df7ce6fe6d6fcd266fd8b (patch) | |
| tree | f49b5a6e223d9073bd9da053d0f20245ab52b193 /engine/termops.ml | |
| parent | efe60d3c1b09bc059053b7383e068ddc05248dac (diff) | |
[dune] [coqide] Use copy action instead of (run cp ...)
This is a bit more portable.
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions