aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools/coqrst
diff options
context:
space:
mode:
authorGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-04-30 09:53:18 -0400
committerGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-05-15 12:05:44 -0400
commita6545a120c6587af38883597d20ac28131b813a9 (patch)
tree5e6f088e8229abd0236c94b60b8516cb24a85331 /doc/tools/coqrst
parentdc5b6e15a2db658fb36754608683b10f847b3e94 (diff)
[doc] Clarify a comment in the README
Diffstat (limited to 'doc/tools/coqrst')
0 files changed, 0 insertions, 0 deletions