Skip to content
Snippets Groups Projects
Commit f645d086 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

don't rename index.html to indexpage.html in coqdocjs target

parent 9fa2acb3
No related branches found
No related tags found
1 merge request!94don't rename index.html to indexpage.html in coqdocjs target
Pipeline #25876 passed
......@@ -6,4 +6,4 @@ htmlpretty: $(GLOBFILES) $(VFILES)
--with-header scripts/coqdocjs/header.html --with-footer scripts/coqdocjs/footer.html \
-html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
$(HIDE)cp scripts/coqdocjs/resources/* html
$(HIDE)mv html/index.html html/indexpage.html
......@@ -18,8 +18,8 @@
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="../../">Project Page</a>
<a href="./index.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
......
......@@ -169,7 +169,7 @@ function fixTitle(){
var url = "/" + window.location.pathname;
var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
if (basename === "toc") {document.title = "Table of Contents";}
else if (basename === "indexpage") {document.title = "Index";}
else if (basename === "index") {document.title = "Index";}
else {document.title = basename;}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment