diff options
| author | Emilio Jesus Gallego Arias | 2018-10-07 07:01:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-29 01:25:34 +0100 |
| commit | 503fa442869978a9e19e738be990ea8c7534962e (patch) | |
| tree | 16e1a42ff9955a80ac6bd1b2302992516b6840ee /gramlib/dune | |
| parent | 06979f87959866e6ed1214e745893dcd2e8ddbb3 (diff) | |
[camlp5] Automatic conversion from revised syntax + parsers
`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
Diffstat (limited to 'gramlib/dune')
| -rw-r--r-- | gramlib/dune | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gramlib/dune b/gramlib/dune new file mode 100644 index 0000000000..f7605fa9f3 --- /dev/null +++ b/gramlib/dune @@ -0,0 +1,4 @@ +(library + (name gramlib) + (public_name coq.gramlib) + (wrapped false)) |