diff options
| author | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
| commit | b424691372a61de64b8b9a8c94ef0c9cb61c7274 (patch) | |
| tree | 60c2cc24ad7550f07cb06aedfb2a3c5402f016ce /kernel/nativecode.mli | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions