diff options
| author | Gaëtan Gilbert | 2020-02-20 14:06:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-20 14:06:59 +0100 |
| commit | 21551b37cfa25657cf51179ad60e9ead455390f0 (patch) | |
| tree | 5e1bede3fcfd169d14a52839765b3ab60a6795aa /dev/ci | |
| parent | 01f8d7666b282b0913ddc266d842d986e12976fa (diff) | |
| parent | 353c5dcda5f9a67e09ac2e7003c4c2a59268641c (diff) | |
Merge PR #11616: [coqdep] Tweak changelog after recent PRs.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions