aboutsummaryrefslogtreecommitdiff
path: root/dev/include_dune
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-16 20:02:06 +0100
committerThéo Zimmermann2019-02-16 20:02:06 +0100
commit355f6eceb666964ad060caf557903d8f82ec1755 (patch)
tree42b26ffa1cdef7934c7b09d9b36740b284a29386 /dev/include_dune
parent0e82d6b1a3006ad260e91c06be9151bfdd406f8e (diff)
Add links for all mentions of Gitter and Discourse.
Update the part about following the development. Remove the reference to Coqdev.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions