From ac6100ebdc75b433d040c7cef3525b78450faf5a Mon Sep 17 00:00:00 2001
From: Tan Yee Jian <tanyeejian@gmail.com>
Date: Mon, 16 Sep 2024 11:14:49 +0200
Subject: [PATCH] Point 'index' in CoqDocJS header to index.html (#1094)

---
 html/resources/header.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/resources/header.html b/html/resources/header.html
index cc81721b4..5a633a782 100644
--- a/html/resources/header.html
+++ b/html/resources/header.html
@@ -19,7 +19,7 @@
 
     <span class="right">
       <a href="../">Project Page</a>
-      <a href="./indexpage.html"> Index </a>
+      <a href="./index.html"> Index </a>
       <a href="./toc.html"> Table of Contents </a>
     </span>
 </div>