diff options
| author | Théo Zimmermann | 2019-03-27 09:51:41 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-27 09:51:41 +0100 |
| commit | 9ad325a9ff3871f46a953e5fd2362f8eab735bdf (patch) | |
| tree | efdffa927b1b1762a46063cedbd3598d538e91cb /kernel/typeops.ml | |
| parent | 2ac275c0f3e65a402951de86a61c77dd0e0782f8 (diff) | |
| parent | 4220af0f8cfbf55bc0ce5fb2d3ddf8657a8807ed (diff) | |
Merge PR #9837: Fix some critical-bugs informations
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions