aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-02-22 09:42:59 -0800
committerGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-02-22 09:42:59 -0800
commitd2293c3e1d51bdd2c25b203c655cc499e9bd5a91 (patch)
treee5754a33f7d64dbed09242b1ea4ab730df7f150e
parent648483fe2ff3942b9f2f2cbbf7a0552b8e1997c4 (diff)
Tweak developer documentation.
-rw-r--r--dev/doc/build-system.txt4
1 files changed, 3 insertions, 1 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 1c4fd2eba..fd3101613 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -143,7 +143,9 @@ file list(s):
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.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+ 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