diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 16:41:56 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 21:35:43 -0400 |
| commit | 7e6b2c6311933f8ef947935f5d4b5897816ab3e4 (patch) | |
| tree | d79e3d7cbc24851164558aa8331b62cddff2eb93 /dev/tools/pre-commit | |
| parent | bab3c8de77486b0cf022d8f8a19e94f588190b7c (diff) | |
[ocamlformat] Use doc-comments=before style.
IMHO it is a bit more logical, WDYT?
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions