From 973dac608117c480c373f9aa90cfa6d7bd46b0cf Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 2 Sep 2024 15:38:19 +0200
Subject: [PATCH] fix links

---
 html-template/index.html | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/html-template/index.html b/html-template/index.html
index 6781b0e..c5b70f5 100644
--- a/html-template/index.html
+++ b/html-template/index.html
@@ -184,7 +184,8 @@ <h1>Import Graph</h1>
   for (let [node, node_data] of graph.nodeEntries()) {
     // In line with the `--exclude-meta` option
     let path = (node == '«Mathlib.Tactics»') ? [node] : node.split('.');
-    node_data.proj = path;
+    node_data.proj = path[0];
+    node_data.full_path = path;
     if (graph.getNodeAttribute(node, 'in_module')) {
       node_data.path = path.slice(1);
       if (path.length <= 1) {
@@ -486,7 +487,7 @@ <h1>Import Graph</h1>
   renderer.on("enterNode", ({ node }) => { setHoveredNode(node);  });
   renderer.on("leaveNode", () => { setHoveredNode(default_hover ? state.defaultNode : undefined); });
   renderer.on("clickNode", ({ node }) => {
-    let path = graph.getNodeAttribute(node, 'path');
+    let path = graph.getNodeAttribute(node, 'full_path');
     window.open(docs_url + path.join('/') + ".html");
   });