diff options
author | 2017-06-05 22:48:45 +0200 | |
---|---|---|
committer | 2017-06-05 22:48:45 +0200 | |
commit | cebab877a73d46628a85fa5d5b0ae1f1bb00d285 (patch) | |
tree | 53cccf63c28f773e40566eea75b233465d425f97 /kernel/sorts.ml | |
parent | c9c9be2c3eb451ac5bcc1bc08f98b3176f29c84d (diff) | |
parent | 54cf593ec1c47ecd5a875714e8e0857707c72901 (diff) |
Merge PR#724: Move README.ci to markdown
Diffstat (limited to 'kernel/sorts.ml')
0 files changed, 0 insertions, 0 deletions