diff options
| author | Théo Zimmermann | 2020-03-26 11:25:10 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-26 11:25:10 +0100 |
| commit | b398a4eb55c42a97d7d177839d5033a306ee7d52 (patch) | |
| tree | 707105889c62bdba854398e10c32df9ffdb470e0 /doc | |
| parent | 63f2da5b3703a16c7722b91ce2f2c78617dec9a7 (diff) | |
| parent | 7e6b2c6311933f8ef947935f5d4b5897816ab3e4 (diff) | |
Merge PR #11832: [ocamlformat] Use doc-comments=before style.
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions