aboutsummaryrefslogtreecommitdiff
path: root/dev/bench/gitlab.sh
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-25 15:57:43 +0000
committerGitHub2020-08-25 15:57:43 +0000
commit51c0d56a5b0384e2f6bd980a1111547641c66b3e (patch)
tree7fc10dc42c27cb2e71c1b75d57e669377059c77a /dev/bench/gitlab.sh
parent3365b1e640e9a9a4694c85d3f988115ce79be9f9 (diff)
parent7da4b8df48d959297e1e4f9e6cc508cf1f0b8be0 (diff)
Merge PR #12879: added numeral_notation to META.coq.in
Reviewed-by: ejgallego Ack-by: Alizter Ack-by: gares
Diffstat (limited to 'dev/bench/gitlab.sh')
0 files changed, 0 insertions, 0 deletions