aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/_CoqProject
diff options
context:
space:
mode:
authorJason Gross2020-08-25 14:56:32 -0400
committerJason Gross2020-09-03 14:15:07 -0400
commitf9eeec7101da55263b644164d1f096af232eb995 (patch)
tree034a851deaf3697148bcc5da23c8252900852cfb /doc/plugin_tutorial/tuto0/_CoqProject
parentf9c37872f559e018f9782b183e4959a0ead03912 (diff)
[bench] Only upload some files
We will now also record a listing of all files that we could have uploaded, in case we want to know what's available to upload in the future.
Diffstat (limited to 'doc/plugin_tutorial/tuto0/_CoqProject')
0 files changed, 0 insertions, 0 deletions