diff options
| author | Emilio Jesus Gallego Arias | 2018-11-07 01:21:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-07 01:21:25 +0100 |
| commit | b39a7c75a9d90b0fa4446fcefd6708d32271dad2 (patch) | |
| tree | 14b6dfe98850241065e4d441e1daf568f587dea4 /tuto2/src/dune | |
| parent | a3e1acb50be3b700b7c36daef4d56f6c6d3ded6a (diff) | |
[dune] Add support for building with Dune for the ML part.
This allows to drop the plugin_tutorials in the coq tree and have the
build compose.
Diffstat (limited to 'tuto2/src/dune')
| -rw-r--r-- | tuto2/src/dune | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/tuto2/src/dune b/tuto2/src/dune new file mode 100644 index 0000000000..f2bc405455 --- /dev/null +++ b/tuto2/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto2_plugin) + (public_name coq.plugins.tutorial.p2) + (libraries coq.plugins.ltac)) + +(rule + (targets demo.ml) + (deps (:pp-file demo.mlg) ) + (action (run coqpp %{pp-file}))) |