Merge remote-tracking branch 'template/more_folder_extension' into...

Merge remote-tracking branch 'template/more_folder_extension' into experimental/template_more_folder

Makefile

@@ -47,7 +47,7 @@ _CoqProject: Makefile
 $(HTMLDIR):
 	mkdir -p $(HTMLDIR)
 
-html: $(HTMLDIR)/index.html
+html: $(HTMLDIR)/toc.html
 
 define GENIndex
 BEGIN {									\
@@ -58,8 +58,8 @@ BEGIN {									\
 }
 endef
 
-$(HTMLDIR)/index.html: $(HTMLDIR)
-	find $(HTMLDIR) -name '*.html' -print0 | xargs -0 basename -a -s .html | grep -Fxv 'index' | awk '$(GENIndex)' > $@
+$(HTMLDIR)/toc.html: $(HTMLDIR)
+	find $(HTMLDIR) -name '*.html' -print0 | xargs -0 basename -a -s .html | grep -Fxv 'toc' | awk '$(GENIndex)' > $@
 
 define GENMakefile
 BEGIN { RS="[[:space:]]"; FS=":" }			\
@@ -78,7 +78,7 @@ BEGIN { RS="[[:space:]]"; FS=":" }			\
 }							\
 END {							\
     print "html:" htmls;				\
-    print HTMLDIR "/index.html: " htmls;		\
+    print HTMLDIR "/toc.html: " htmls;		\
 }
 endef