fix compatibility with --exclude-meta

leanprover-community · Sep 2, 2024 · 0a6ed6c · 0a6ed6c
1 parent 457d10b
commit 0a6ed6c
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/html-template/index.html b/html-template/index.html
@@ -182,7 +182,8 @@ <h1>Import Graph</h1>
 
   // unpack the node labels into data
   for (let [node, node_data] of graph.nodeEntries()) {
-    let path = node.split('.');
+    // In line with the `--exclude-meta` option
+    let path = (node == '«Mathlib.Tactics»') ? [node] : node.split('.');
     node_data.proj = path;
     if (graph.getNodeAttribute(node, 'in_module')) {
       node_data.path = path.slice(1);