diff options
author | 2016-10-05 18:18:22 +0200 | |
---|---|---|
committer | 2016-10-05 18:18:22 +0200 | |
commit | 2dcd8f2e82366bb3b0f51a42426ccdfbb00281dc (patch) | |
tree | 4e9a44599dec13e262538e70a6a60bcf3e5fa97e /kernel/term.ml | |
parent | 01a448be0133872a686e613ab1034b4cb97cd666 (diff) | |
parent | 8114da3ba8a9b31ffe194e7f7f0239ecc2219b9c (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'kernel/term.ml')
0 files changed, 0 insertions, 0 deletions