aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-25 17:13:13 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-25 17:13:13 +0200
commit6d4d16eb5518a9fb461e0f0433c9ce54d2197158 (patch)
treeee9249b420e41ff864da77b65ba0ee467d983306 /.circleci
parentc97a4b7bb4af07c22137e0933d041d1f7eea95f1 (diff)
parent38fbc6e523bb45aa18761dbb027bc1ae479632cd (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