aboutsummaryrefslogtreecommitdiffstats
path: root/tools
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-02-08 16:44:06 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-02-08 16:44:06 +0100
commitf80498e19a670040dce0795a8ea1cc83ca490ecc (patch)
tree158483ab5559938537983d8e2f1640457ddbfe47 /tools
parentf02f00a01b598567f70e138c144d9581973802e6 (diff)
downloadcompcert-kvx-f80498e19a670040dce0795a8ea1cc83ca490ecc.tar.gz
compcert-kvx-f80498e19a670040dce0795a8ea1cc83ca490ecc.zip
Extend the modorder tool to handle Coq files as well (#54)
This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs. Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
Diffstat (limited to 'tools')
-rw-r--r--tools/modorder.ml16
1 files changed, 9 insertions, 7 deletions
diff --git a/tools/modorder.ml b/tools/modorder.ml
index 34e157d0..d1203568 100644
--- a/tools/modorder.ml
+++ b/tools/modorder.ml
@@ -29,7 +29,7 @@ type node = {
let re_continuation_line = Str.regexp "\\(.*\\)\\\\[ \t]*$"
-let re_depend_line = Str.regexp "\\([^ ]+\\) *:\\(.*\\)$"
+let re_depend_line = Str.regexp "\\([^:]*\\):\\(.*\\)$"
let re_whitespace = Str.regexp "[ \t\n]+"
@@ -51,12 +51,14 @@ let parse_dependencies depfile =
end else begin
let lhs = Str.matched_group 1 l
and rhs = Str.matched_group 2 l in
- let node = {
- deps = Str.split re_whitespace rhs;
- result = rhs;
- status = Todo
- } in
- Hashtbl.add deps lhs node
+ let lhs = Str.split re_whitespace lhs
+ and rhs = Str.split re_whitespace rhs in
+ List.iter (fun lhs -> let node = {
+ deps = rhs;
+ result = lhs;
+ status = Todo
+ } in
+ Hashtbl.add deps lhs node) lhs
end in
begin try