aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-07 17:44:22 +0000
committerGitHub2021-04-07 17:44:22 +0000
commit59d0462f35818c12a0727a560d7b9ecf2ceea994 (patch)
tree5b01de7e969b000fa64cc7edca60323eb11958d7 /plugins/funind
parentd98faea005d32b64252bf6bd50eb01f320a2bc8c (diff)
parent7769a1f12baa19ef1d0bccb4db36168f0fe0dcc1 (diff)
Merge PR #14032: CI: don't output-sync
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions