diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 09:59:44 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 09:59:44 +0100 |
| commit | 374e105be93beb2e9353bedf5cdd700a26308ebd (patch) | |
| tree | 5ffbb6fb23e3d418ed7d3eaec5360c7a69de9c1e /dev/doc | |
| parent | aec08b873425f6cdae4e1434651b4e9a97d0ced0 (diff) | |
| parent | d2293c3e1d51bdd2c25b203c655cc499e9bd5a91 (diff) | |
Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_state.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.txt | 4 |
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 |