diff options
| author | Emilio Jesus Gallego Arias | 2019-03-28 17:18:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-28 17:18:25 +0100 |
| commit | 5408978c2ed5ffb4da885f742cd808bc0b518021 (patch) | |
| tree | 0fb04cf648a7fc0a81f9d41eeda4a39a11658ccf /doc/plugin_tutorial/README.md | |
| parent | 688e20c432d2639050a62703e1c566ddfbe42b2a (diff) | |
[dune] Fix shim quoting and add coqc wrapper.
The quoting was incorrect thus scripts didn't properly work.
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions