diff options
| author | Maxime Dénès | 2018-10-29 13:56:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-29 13:56:41 +0100 |
| commit | 765c61d42e301c1f98c44b3986d73a052ca3a8c5 (patch) | |
| tree | 29357e72db169736b51acb80214fa4a93d156fe9 /kernel/reduction.ml | |
| parent | 35f715a005063a2c6195c574d019ba202bcdc27b (diff) | |
| parent | 7bf7d431eaf1fe5d522ae41028f065d5c33b866d (diff) | |
Merge PR #8765: Give code ownership of merging doc to pushers team to notify members when it changes.
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions