Various fixes in the Makefiles

 After a successful build, re-doing make world should almost do nothing.
 For that:
  - Many targets added to .PHONY, especially "tools" since a "tools"
    directory exists. And anyway this is said to speed-up make a bit.
  - Concerning fake_ide, mentionning the .cm* instead of the .ml*
    avoid rebuilding these .cm*, and hence possibly many other things.
  - in Makefile.doc: fix the rule building index_url.txt
  - coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP)
    (which is the symlink). This avoids a situation where a first
    "make" could redo just a few files while a second "make" will
    rebuild many more. Typical scenario : touch the Makefile,
    1st make was re-doing tolink.ml and then coqmktop, but no more,
    a 2nd make was then detecting that coqtop and the stdlib was to
    be redone

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 14 deletions

diff --git a/Makefile.doc b/Makefile.doc
index dc3ae8b5f..42f9bf7aa 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -11,9 +11,12 @@
 ### General rules
 ######################################################################
 
-.PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial
+.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial
+.PHONY: stdlib full-stdlib faq rectutorial
 
-doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt
+INDEXURLS:=doc/refman/html/index_url.txt
+
+doc: refman faq tutorial rectutorial stdlib $(INDEXURLS)
 
 doc-html:\
   doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
@@ -120,8 +123,11 @@ doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html
 doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
 	$(INSTALLLIB) $< doc/refman
 
-doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
-                        doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
+INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
+ALLINDEXES:= doc/refman/html/index.html $(INDEXES)
+
+$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+	       doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
 	- rm -rf doc/refman/html
 	$(MKDIR) doc/refman/html
 	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
@@ -136,6 +142,14 @@ refman-quick:
 	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
 
 ######################################################################
+# Index file for CoqIDE
+######################################################################
+
+doc/refman/html/index_url.txt: $(INDEXES)
+	cat $< | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > $@
+
+
+######################################################################
 # Tutorial
 ######################################################################
 
@@ -281,16 +295,6 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
 	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
 
 ######################################################################
-# Index file for CoqIDE
-######################################################################
-
-# Not robust, improve...
-ide/index_urls.txt: doc/refman/html/index.html
-	@ rm -f doc/refman/html/index_urls.txt
-	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > doc/refman/html/index_urls.txt
-
-
-######################################################################
 # Install all documentation files
 ######################################################################