diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index 0c14f2354..da5e8e694 100644 --- a/Makefile.build +++ b/Makefile.build @@ -701,6 +701,9 @@ ml-doc: parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) +parsing/grammar.dot : | parsing/grammar.mllib.d + $(OCAMLDOC_MLLIBD) + tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d $(OCAMLDOC_MLLIBD) |