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 6203dd759..064f89aa0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -53,7 +53,7 @@ world: coq coqide documentation revision coq: coqlib coqbinaries tools -# Note: 'world' do not build the bytecode binaries anymore. +# Note: 'world' does not build the bytecode binaries anymore. # For that, you can use the 'byte' rule. Native and byte compilations # shouldn't be done in a same make -j... run, otherwise both ocamlc and # ocamlopt might race for access to the same .cmi files. |