diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/build-system.txt | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index b243ebe2ed..d7cf396ff5 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -108,9 +108,6 @@ save precious time: like that. This will avoid entering the stage 3, and cut build system overhead by 50% (1.2s instead of 2.4 on writer's machine). - - You can turn off rebuilding of the standard library each time - bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1. - - If you want to avoid all .ml4 files being recompiled only because grammar.cma was rebuilt, do "make ml4depclean" once and then use NO_RECOMPILE_ML4=1. |