aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-01 19:39:44 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-01 19:39:44 +0000
commit5e88ae6b465f38da8e6864626e23673a14927c10 (patch)
tree210b4c847b9397006b9a1df4364739d6cc61c821 /Makefile.common
parenteddd2aa6686789ef4ebfcd0f1713fd4a283b111f (diff)
Quelques amendements liées à la compilation des packages.
- typo du configure; - warnings variables non utilisées dans ide/utils; - suppression des variables vides COQINSTALLPREFIX et OLDROOT parce que l'option -e que l'on aurait pu en principe utiliser pour les surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux d'imbrication de makefiles (comme c'est le cas quand on vient du makefile servant à faire les packages qui appelle le makefile principal qui appelle les makefile.stage); - utilisation de ALLVO plutôt qu'un find pour trouver les .v sur lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers de test, non prévus pour faire partie de la biblio standard); - utilisation de -custom sur les bytecode qui ne l'étaient pas encore (coqchk et coqmktop) pour être indépendant de ocamlrun à l'installation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index b76e9aaf6..cba65055a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -812,6 +812,7 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
$(SUBTACVO) $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+VFILES:= $(ALLVO:.vo=.v)
LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
LIBFILESLIGHT:=$(THEORIESLIGHTVO)