Merge PR #8754: [doc] [build] Remove ocamlbuild leftovers.

1 files changed, 3 insertions, 5 deletions

diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index fd3101613a..8cefe699cc 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -140,11 +140,9 @@ New files
 For a new file, in most cases, you just have to add it to the proper
 file list(s):
  - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
-   These files are also used by the experimental ocamlbuild plugin,
-   which is quite touchy about them : be careful with order,
-   duplicated entries, whitespace errors, and do not mention .mli there.
-   If module B depends on module A, then B should be after A in the .mllib
-   file.
+   Be careful with order, duplicated entries, whitespace errors, and
+   do not mention .mli there.  If module B depends on module A, then B
+   should be after A in the .mllib file.
 - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build