diff options
| author | Gaëtan Gilbert | 2018-10-30 21:44:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 21:44:25 +0100 |
| commit | d32301dde8071acc914286c675b9749e27f368d2 (patch) | |
| tree | cafcad3409648e40c44bcb8c3923885b5785157d /kernel/typeops.mli | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
| parent | b33794516f4dd10edcb06be49c0202a9e056c26e (diff) | |
Merge PR #8750: [ci] [doc] Notes about branch names.
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions