aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-20 17:25:20 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-20 17:25:20 +0000
commitac98362d168bc96433bf09ced8ee992bce76483e (patch)
tree386b04b0310a96bd05488741b7da0b69d1286561 /Makefile
parent5e8ebbc13909125093e2c7aa18e00cf30cad6362 (diff)
Remove broken makefile option NO_RECOMPILE_LIB
The idea was to allow rebuilding coqtop without the whole stdlib, but it's not working anymore since the stdlib also depends on plugins .cmxs, hence its compilation will be triggered anyway. Since I've no idea how to restore the old behavior (except via hacking the output of coqdep with more ORDER_ONLY hack), I simply declare this option dead, and remove it for improving clarity. NB: an imperfect workaround is to touch all the .vo after rebuilding coqtop and the plugins... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index ca8022cde..40de0536c 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,6 @@
#
# make VERBOSE=1 # restore the raw echoing of commands
# make NO_RECALC_DEPS=1 # avoid recomputing dependencies
-# make NO_RECOMPILE_LIB=1 # a coqtop rebuild does not trigger a stdlib rebuild
#
# Nota: the 1 above can be replaced by any non-empty value
#