diff options
| author | Clément Pit-Claudel | 2019-10-15 16:05:53 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-10-15 16:05:53 -0400 |
| commit | 5a679b6c808188dd2bf9b600843f35a52a400d3c (patch) | |
| tree | 612dfb9acc5184e741074cf8ab42b340925d6989 /kernel/type_errors.ml | |
| parent | 911accd83d0161d1587652af9ec5365943023c98 (diff) | |
| parent | 465eee6300dd49f207af05485789a2f855f3ea74 (diff) | |
Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.
Ack-by: SkySkimmer
Reviewed-by: cpitclaudel
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions