diff options
| author | Emilio Jesus Gallego Arias | 2020-03-29 13:39:07 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-29 13:39:07 -0400 |
| commit | 6760a066168a5be0d3b479741fe8ac6c39339610 (patch) | |
| tree | cb6c1352ae5934dd11130400672034293ad88e46 /configure.ml | |
| parent | 8d1382b996d9421162839c3f481e866fef06fd41 (diff) | |
| parent | 6f488ef6c1f678661828ce0509ec79feaa1599df (diff) | |
Merge PR #11938: Support for updating orderedGrammar with Dune.
Reviewed-by: ejgallego
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions