diff options
| author | Hugo Herbelin | 2019-05-21 12:08:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-21 12:08:44 +0200 |
| commit | 897088fb8f4769bacca9fc289387096283835cd6 (patch) | |
| tree | 2934fbca8e3e803e445f84cb65ecf7986c271f50 /kernel/nativecode.mli | |
| parent | a5304d0a613141dd5008410034ae4b104f0fc06a (diff) | |
| parent | 076932d4bf602560b24c14dc3397e51db5114244 (diff) | |
Merge PR #10144: Fix #9919: conversion functions are non-linear
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions
