diff options
| author | Théo Zimmermann | 2018-08-01 10:58:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-01 10:58:18 +0200 |
| commit | 2dcb340f82c3df70d8fe2c6acc3536913a86144a (patch) | |
| tree | 86e627cb4c13ec2b1533c557224495ed1d15908e /kernel/type_errors.ml | |
| parent | 29a432dfbaa83dd1459c7af95f556555da15a1ce (diff) | |
| parent | 7f1ed3298c841c2afa4faf080a5f65361bbb413f (diff) | |
Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a title
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions