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 /dev/doc | |
| 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 'dev/doc')
0 files changed, 0 insertions, 0 deletions