fix links

leanprover-community · Sep 2, 2024 · 973dac6 · 973dac6
1 parent cad64a5
commit 973dac6
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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");
   });