diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-18 11:08:26 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-18 11:08:26 -0400 |
| commit | 26d2171060daf642008fd2430c8f78b8f7b9c43c (patch) | |
| tree | 22b46daa6235613effea9f76a5666a579a1bbd0c /pretyping/classops.mli | |
| parent | 0daf6af5949dbc7304e9fc3adf063519d5a60c4b (diff) | |
| parent | e43461e841bb8a92fca7414013d88319b9b84ed5 (diff) | |
Merge PR #7855: Update section on adding your project to CI and link to example PR.
Diffstat (limited to 'pretyping/classops.mli')
0 files changed, 0 insertions, 0 deletions