Add documentation to index.md

coq-community · Dec 22, 2020 · 3867b19 · 3867b19
1 parent 6d0eada
commit 3867b19
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/index.md.mustache b/index.md.mustache
@@ -55,3 +55,5 @@ Related publications, if any, are listed below.
 {{# authors }}
 - {{& name }}
 {{/ authors }}{{& after_authors }}
+
+{{& documentation }}
diff --git a/ref.yml b/ref.yml
@@ -370,9 +370,10 @@ fields:
   - documentation:
       required: false
       description: >
-        The part of the README that is not auto-generated.
+        The part of the README and index that is not auto-generated.
       used:
         - README.md
+        - index.md
   - coqdoc_index:
       required: false
       description: Position of Coqdoc main page relative to index