diff options
| author | Hugo Herbelin | 2018-04-13 19:47:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:27:50 +0200 |
| commit | 09482343fec8cd40b1f9523be8e5e2601eb0bbae (patch) | |
| tree | c03215fd6c6ef1416b159a33d59abc87d976a1b1 /plugins/syntax/plugin_base.dune | |
| parent | a25a28e167aabca816a6af37c69a1a72a6be9388 (diff) | |
Minor cosmetic unifying of layout in pretyping.ml.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions