diff options
| author | Maxime Dénès | 2018-05-15 10:31:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-15 10:31:31 +0200 |
| commit | cfed57b021b89018d1bb30c6aa0957299fe35d8d (patch) | |
| tree | 08c656b3146dfca02288ade499de1db2de127f00 /dev/ci/ci-common.sh | |
| parent | 3a0dfe68e14f8f5e40cc56c3bb0c583318debeb5 (diff) | |
| parent | d5a352faa11576d2eda294ca6872d543b0e695da (diff) | |
Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.
Diffstat (limited to 'dev/ci/ci-common.sh')
0 files changed, 0 insertions, 0 deletions