From ca4775a3b2cfdc0ab3ae12f453892a82aec048b1 Mon Sep 17 00:00:00 2001
From: lmamane
Date: Wed, 13 Feb 2008 15:21:17 +0000
Subject: Implement NO_RECALC_DEPS option in build system

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/build-system.txt | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 5b71dc9c92..e4ecf9e5f6 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -84,6 +84,12 @@ save precious time:
    build system dares to), use GOTO_STAGE=n. This will jump into stage
    n and try to do the targets you gave in that stage.
 
+ - To disable all dependency recalculation, use the NO_RECALC_DEPS=1
+   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.
+
 Dependencies
 ------------
 
-- 
cgit v1.2.3