diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-25 17:13:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-25 17:13:13 +0200 |
| commit | 6d4d16eb5518a9fb461e0f0433c9ce54d2197158 (patch) | |
| tree | ee9249b420e41ff864da77b65ba0ee467d983306 /.circleci | |
| parent | c97a4b7bb4af07c22137e0933d041d1f7eea95f1 (diff) | |
| parent | 38fbc6e523bb45aa18761dbb027bc1ae479632cd (diff) | |
Merge PR #6866: Slight improvement of messages related to direct and indirect uses of tactic `clear`.
Diffstat (limited to '.circleci')
0 files changed, 0 insertions, 0 deletions