aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-10 13:57:38 +0000
committerGitHub2021-03-10 13:57:38 +0000
commitcde4dceb93ba1f91d20f13a0fdea8f9731a6a626 (patch)
tree92ff2503b55f731c3ef80c7f56150b98952aad68 /dev/base_include
parent317db327c21ac78bd921020118b19afaf1c02350 (diff)
parent9955d2dfe778e41e447cb3ae71e708c7a3716f0d (diff)
Merge PR #13901: Fix list contributors
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions