diff --git a/scripts/coqdocjs/Makefile.coqdocjs b/scripts/coqdocjs/Makefile.coqdocjs index 37f22596a79b34f14d103f6c5d31de560b61bdb0..00282dde79f3225c94aa0299778a596c6ed0f42e 100644 --- a/scripts/coqdocjs/Makefile.coqdocjs +++ b/scripts/coqdocjs/Makefile.coqdocjs @@ -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 + diff --git a/scripts/coqdocjs/header.html b/scripts/coqdocjs/header.html index cc81721b4911be4187ac85cc7125b5c04175d40c..0244c7919057886d4ba3bf314eed82878f79752c 100644 --- a/scripts/coqdocjs/header.html +++ b/scripts/coqdocjs/header.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> diff --git a/scripts/coqdocjs/resources/coqdocjs.js b/scripts/coqdocjs/resources/coqdocjs.js index 10dc0bb6524872d2ba2a2a417fc6c3611191f6b3..3da2050782df8e565e33cf030689b72c935dd14d 100644 --- a/scripts/coqdocjs/resources/coqdocjs.js +++ b/scripts/coqdocjs/resources/coqdocjs.js @@ -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;} }