aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1
diff options
context:
space:
mode:
authorClément Pit-Claudel2019-06-12 11:21:59 -0400
committerClément Pit-Claudel2019-06-12 11:21:59 -0400
commitac854a5542b2118be5dfd7bd26d9e3a5db945167 (patch)
treeb8244b8a4feda26e3ccc431209396716f2fa5252 /doc/plugin_tutorial/tuto1
parentc049fa922fd1a12a4a5faddcd06b3475d0529cf6 (diff)
parenta3da7880393791fcf3ed3eafe8444b3049e3119f (diff)
Merge PR #10310: Fix #10283: clearer dependency documentation for building CoqIDE.
Reviewed-by: cpitclaudel Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions