diff options
| author | Matej Kosik | 2016-10-12 16:37:16 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-10-19 13:48:52 +0200 |
| commit | ad81c04a923c594b7a893f08bb5571a6db74c92a (patch) | |
| tree | 7ddd1090d6874c644d6e1f4633bb7e0e7d592502 /interp/implicit_quantifiers.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 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions
