diff options
| author | Maxime Dénès | 2018-08-16 15:44:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-08-16 15:44:55 +0200 |
| commit | cf1721c368277015c80a5feb6cb0bcad3f93566e (patch) | |
| tree | 1c0e1b0898c6e6136563fb6cfe24b8e70ce842b9 /kernel/type_errors.ml | |
| parent | 71aa2992f4e8a6eb2bc64ecf9aa40a9b0bc0f233 (diff) | |
| parent | ec817cc2809a69bfff3c26353d1dc64ac59fe30b (diff) | |
Merge PR #8079: Document the automatic use of the rebase label.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions