diff options
| author | Emilio Jesus Gallego Arias | 2020-03-25 21:48:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 21:48:16 -0400 |
| commit | 1217583de0c7ac0d17c8917f21c30c247176d83f (patch) | |
| tree | 43df44614d49c69c774ca0175c69173ecdb160a5 /plugins/syntax/plugin_base.dune | |
| parent | bab3c8de77486b0cf022d8f8a19e94f588190b7c (diff) | |
| parent | 5e3e9507f890c01e1c48ce3b8014257ffd9a0931 (diff) | |
Merge PR #11898: Switch opam file to make
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions