diff options
| author | Pierre-Marie Pédrot | 2020-02-08 13:14:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-08 13:14:20 +0100 |
| commit | 80010afc70eee3df65b6f8a16a202fb9da11fb80 (patch) | |
| tree | f7251eb90109afb1e12f799bb87ea06791ebf302 /kernel/nativecode.ml | |
| parent | 79e9700d0533c3f36c9fbf0011f816981b8a3a3d (diff) | |
| parent | 0fe99a0d6a4d643cf311200c870aeaff042d7069 (diff) | |
Merge PR #11404: replace RList by list R in all files where it is used in this directory
Ack-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions