diff options
| author | Théo Zimmermann | 2020-11-09 16:28:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 16:41:57 +0100 |
| commit | c0b48997dc7fccd15ab237df6274dbcfa05cbc9c (patch) | |
| tree | 681ac33f33677e3bd6ba3b893132eb6caa794a1a /kernel/nativelib.mli | |
| parent | d2047c6368ae11a3a3fd7f2db8c991d135094e60 (diff) | |
Fix indentation of todo in Ltac chapter.
Actual documentation was interpreted as a comment.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions