aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-01-26 10:42:52 +0000
committerGitHub2021-01-26 10:42:52 +0000
commit14051337936db1f56dc052a6e54e5b606552141b (patch)
tree34297481bacc42c31a110ceda19eb4e43061cd0d /plugins
parentcb5e21268ca0da4d26c3ea7e129b1af89d799a8c (diff)
parent3a32f852a0b82c964fad00f57abcacbb90bbee7f (diff)
Merge PR #13773: Add missing item about PDF manual to release checklist.
Reviewed-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions