diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 35f5e26272..ed4cde2b16 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ coq.timing.diff: coqlib.timing.diff # shouldn't be done in a same make -j... run, otherwise both ocamlc and # ocamlopt might race for access to the same .cmi files. -byte: coqbyte coqide-byte pluginsbyte printers +byte: coqbyte coqide-byte pluginsbyte printers bin/votour.byte .PHONY: world coq byte world.timing.diff coq.timing.diff |