aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
authorThéo Zimmermann2020-11-16 10:21:34 +0100
committerGitHub2020-11-16 10:21:34 +0100
commit7b8da8cb0327f3bc5c008b76a29cf4e05585e2ae (patch)
treedb091b62fe7f8b08c37630bd75e88f1ca43bf1b0 /plugins/ltac
parent51ddbbe05ab2c47a2c50c1e6781b8562b7717110 (diff)
Slight improvement to the changelog entry.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions