aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0
diff options
context:
space:
mode:
authorJason Gross2020-04-08 11:08:30 -0400
committerJason Gross2020-04-08 11:08:30 -0400
commitf06d96687e26d3e491de0a234e889e901b32e1ca (patch)
tree13d2f37d57b4e875e6f5e65514d8cdd563c1c497 /doc/plugin_tutorial/tuto0
parentb26d1f477990d88e235ffda0f23f494456ce5862 (diff)
Fix a typo in CoqMakefile.in
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions