diff options
author | Matej Kosik <matej.kosik@inria.fr> | 2016-10-12 16:37:16 +0200 |
---|---|---|
committer | Matej Kosik <matej.kosik@inria.fr> | 2016-10-19 13:48:52 +0200 |
commit | ad81c04a923c594b7a893f08bb5571a6db74c92a (patch) | |
tree | 7ddd1090d6874c644d6e1f4633bb7e0e7d592502 /library/nameops.ml | |
parent | 69401acbe52773a9bef66667587437596f1ea36c (diff) |
Converting certain "order-only" (Makefile) dependencies to regular dependencies.
For some reason "grammar/grammar.cma" was declares only an "order-only" dependency for "*.ml" files generated from "*.ml4".
I this that this is a problem because when we change "grammar/*.mlp" files, even tough "grammar/grammar.cma" is regenerated,
the actual "*.ml" files (defined by "*.ml4" as well as "grammar/grammar.cma") are not regenerated.
Diffstat (limited to 'library/nameops.ml')
0 files changed, 0 insertions, 0 deletions