diff options
| author | Théo Zimmermann | 2019-05-07 14:18:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-07 14:18:51 +0200 |
| commit | 403f8784706d54e5e91bf20e56b0bf8ea40f4df3 (patch) | |
| tree | b265ee33a8ec49cc86d9d28686c72a9722bae787 /kernel/nativecode.mli | |
| parent | c828bca2c11d83a329facd56051abd4d27e16850 (diff) | |
| parent | 590ee35546f3528ac7ccb32306fb86e78fdce93b (diff) | |
Merge PR #10053: Document change_no_check variants
Ack-by: JasonGross
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions