diff options
| author | Théo Zimmermann | 2019-02-14 10:08:34 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-14 10:08:34 +0100 |
| commit | 10443666879e250a36441540b49d311b2b52e03a (patch) | |
| tree | 4665ff837588666a5ded07356d9d683b93495cd9 /kernel/nativecode.ml | |
| parent | 0e36b06e8426d2fcd18fafed187a676ceb6592ae (diff) | |
| parent | 5446b141fb94fcbc5b05a0ef8ec362fd7485e91e (diff) | |
Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaning
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions