diff options
author | lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-05 13:43:01 +0000 |
---|---|---|
committer | lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-05 13:43:01 +0000 |
commit | 49a0d1c36fee57db25c65ebfa71e46cf8b103eab (patch) | |
tree | 89cea1152eb31b0b2bd21eda011959b86d19a141 /dev/doc/build-system.txt | |
parent | 73a0a2297ca3c91ccaaa8d2599ea8d6da9eb932e (diff) |
Fix typos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11054 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/build-system.txt')
-rw-r--r-- | dev/doc/build-system.txt | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index f43e21963..c9571f7c9 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -88,13 +88,13 @@ save precious time: option. It disables REcalculation of dependencies, not calculation of dependencies. In other words, if a .d file does not exist, it is still created, but it is not updated every time the source file - (e.g. .ml) is changes. + (e.g. .ml) is changed. General speed improvements: - When building both the native and bytecode versions, the KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time - by running camp4o only once on every .ml4 file, at the expense of + by running camlp4o only once on every .ml4 file, at the expense of readability of compilation error messages for .ml4 files. Dependencies |