aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/_CoqProject
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-12 14:49:25 +0000
committerGitHub2020-11-12 14:49:25 +0000
commit176faf135778471e70a8d47387f9e7d05815609e (patch)
treed5c5bb470e47a9c457f41dade752d2e8238d228e /doc/plugin_tutorial/tuto1/_CoqProject
parent6d7877829b7265d6c416c17ea3bbacf65f306609 (diff)
parent0cbd6c27cd66ee5517db0d4ecbd86dab80d12763 (diff)
Merge PR #13359: Print failed test suite logs in CI
Reviewed-by: ejgallego Reviewed-by: herbelin
Diffstat (limited to 'doc/plugin_tutorial/tuto1/_CoqProject')
0 files changed, 0 insertions, 0 deletions