forked from xavierleroy/coq2html
-
Notifications
You must be signed in to change notification settings - Fork 4
Open
Description
There is a problem that links do not work correctly unless the graph name is “depend” as shown below in the graph dot file given by the option hierarcy-graph, which displays dependent graphs.
Example of a dotfile that does not work properly
digraph foo {
...
}Because the graph name foo of the dot file is not “depend”, the link in the dependent graph does not work properly in the generated html.
How to fix it
The generate_dependency_graph function in generate_index.ml specifies a map by usemap in the img tag. It would be better to use the graph name of the given dot file instead of a constant.
let generate_dependency_graph xref_table output_dir dot_file =
...
Printf.sprintf {|<h2>Clickable Dependency Graph of Files</h2><img src="%s" usemap="#depend" class="img-darkmode-enable"/>%s|} png_filename mapReactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels