aboutsummaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-28 07:24:10 +0000
committerGitHub2021-02-28 07:24:10 +0000
commit7b326354b32868750b3e3ce99b8dc9a3377909ba (patch)
tree3967612b2933809457ad509848d2af6e3661e44f /.github
parentca38bf53deed39c716a911b8d288f91eb334452e (diff)
parentddd4ffea1dd58cd3e50c188699684b7506ce3bee (diff)
Merge PR #13886: Correct broken link.
Reviewed-by: Zimmi48
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions