aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-12 00:11:43 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-12 00:11:43 +0200
commitb6a68f67897819db729e43c1d9b6ecf2c3c77407 (patch)
tree3214a2e5d90e97c449978fa54688007500a2c3a1 /tools/coqdep.ml
parent80b23d020c938a2c06654c8bb0cd15c806e6a582 (diff)
Fixing the undocumented -dumpgraphbox option of coqdep.
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ea5eb02c1..1517121bf 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -382,9 +382,9 @@ let rec insert_graph name path graphs = match path, graphs with
let print_graphs chan graph =
let rec print_aux name = function
| [] -> name
- | (Element str) :: tl -> fprintf chan "%s\n" str; print_aux name tl
+ | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl
| Subgraph (box, names) :: tl ->
- fprintf chan "subgraph cluster%n {\n label=\"%s\"" name box;
+ fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box;
let name = print_aux (name + 1) names in
fprintf chan "}\n"; print_aux name tl
in
@@ -404,7 +404,7 @@ let rec pop_last = function
let get_boxes path = pop_last (split_path path)
let insert_raw_graph file =
- insert_graph (basename_noext file) (get_boxes file)
+ insert_graph file (get_boxes file)
let rec get_dependencies name args =
let vdep = treat_coq_file (name ^ ".v") in