diff --git a/html-template/index.html b/html-template/index.html index 5ffa663..a722d4d 100644 --- a/html-template/index.html +++ b/html-template/index.html @@ -182,7 +182,8 @@

Import Graph

// 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);