diff options
| author | Pierre-Marie Pédrot | 2020-05-25 19:25:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-25 19:25:22 +0200 |
| commit | 2100a8b5d8de37b45ba35028f2d66cedf9c8ad77 (patch) | |
| tree | ae3c6179ad014f6d9799e3ea41141c665810d900 /dev/ci/docker/bionic_coq | |
| parent | 85694cfd5b6308967d98c0266b1ca13aef9375c3 (diff) | |
| parent | 465e9d7b3b8c411c772f93434d0785adea4d15dc (diff) | |
Merge PR #12344: Cleanup noisy prefixes
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci/docker/bionic_coq')
0 files changed, 0 insertions, 0 deletions