aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2018-03-23 15:56:23 +0100
committerThéo Zimmermann2018-03-23 15:56:23 +0100
commit9236c0c40203f132eaa09436b0379d6dde23ddbe (patch)
tree902010b0edac3c1c4e20a318fccd718d25197ec1 /kernel/nativelambda.mli
parent4e3819425445c3236f6aca77e95f2ee854cf4417 (diff)
parentee62b9269beb78b12f1431816ea1acc0cd09130c (diff)
Merge PR #7052: More precise wording about the merge process.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions