diff options
| author | Théo Zimmermann | 2018-07-10 11:12:55 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-10 11:12:55 +0200 |
| commit | f796ad268922e167e2156de0b5beef4eeb001700 (patch) | |
| tree | ff5e1f830413739200707cae5daff5bf82f10004 /kernel/type_errors.mli | |
| parent | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (diff) | |
| parent | 0801250ff9aec71a2ccc2e0227d8706e1fbac6be (diff) | |
Merge PR #8025: Fix rst syntax for `quote ident {ident}`
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions