aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 19:55:10 +0200
committerThéo Zimmermann2020-05-13 19:55:10 +0200
commit4f71e81915a038c8e4d7920822c681c65d500ff2 (patch)
tree7bc64b978d9a2c02ab6857182e1b02d15d36e27c
parentfc29e2d171dea78253cb8e11b59eff20a86c0649 (diff)
Add match to new file on Variants.
-rw-r--r--doc/sphinx/language/core/variants.rst (renamed from doc/sphinx/language/gallina-specification-language.rst)0
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/core/variants.rst
index d9e2c07951..d9e2c07951 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/core/variants.rst