aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-08 21:10:12 +0200
committerPierre-Marie Pédrot2019-06-25 17:38:35 +0200
commit3d9f2d1cbc6256c48523db00fa2cc9743a843dfe (patch)
tree99b6148793f19e4becc581e047c336462b5b3610 /plugins
parentc3efcc501e140a74a948513a0e45223e4d5b521c (diff)
Documenting the Ltac2 change.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions