diff options
| author | Emilio Jesus Gallego Arias | 2018-06-07 13:27:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-07 13:27:57 +0200 |
| commit | 54abefa048519c160c61f0f1c217d658ad0d3aaa (patch) | |
| tree | eb13dcdf8c9b0fae233c8865bf0546664b534d81 /kernel/cbytecodes.ml | |
| parent | 28ca5295339afecfc4ecb70214f6f575c11e34a1 (diff) | |
| parent | adfc3cebf405f599292c7c8f131620837f0af93f (diff) | |
Merge PR #7735: Remove cross-crypto from Travis. It is still tested in GitLab CI.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions
