diff options
| author | Gaëtan Gilbert | 2020-04-13 16:41:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 16:41:03 +0200 |
| commit | b8fcbecf8e1b96dcb47f15ac7573197de43f0bdb (patch) | |
| tree | 58555d9bcf80eba6b0efe56ef6ffd5ba3a59cd28 /dev/ci/docker | |
| parent | 0beca74bc90cef03d779a8e4f8668335c9c37716 (diff) | |
| parent | cb35474d6d55f353745c0cd470d76a72c352c9d2 (diff) | |
Merge PR #12081: [test-suite] Remove deprecated -I option of coqchk in Makefile
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions