diff options
| author | Ambroise | 2018-06-28 14:52:36 +0200 |
|---|---|---|
| committer | Ambroise | 2018-06-28 14:52:36 +0200 |
| commit | 5b96722d51026c47fe569df85a5ffc4d14397d12 (patch) | |
| tree | 51557da0345b29b577650a6549255b63102c9eb7 /kernel/type_errors.mli | |
| parent | f00843701373257c069d33e84b78ecaeae9e4cb0 (diff) | |
wrong sphinx syntax
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions