From f645d0862b95857f5b65610a02612da0a4cdf7d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 31 Mar 2020 12:44:59 +0200
Subject: [PATCH] don't rename index.html to indexpage.html in coqdocjs target
---
scripts/coqdocjs/Makefile.coqdocjs | 2 +-
scripts/coqdocjs/header.html | 4 ++--
scripts/coqdocjs/resources/coqdocjs.js | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/scripts/coqdocjs/Makefile.coqdocjs b/scripts/coqdocjs/Makefile.coqdocjs
index 37f22596a..00282dde7 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 cc81721b4..0244c7919 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 10dc0bb65..3da205078 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;}
}
--
GitLab