aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorherbelin2005-12-26 17:05:45 +0000
committerherbelin2005-12-26 17:05:45 +0000
commit989718e36ca338a64c248723d2590bb3eb4854a5 (patch)
tree455e904dbaab380b0fb8a6949bb0af26370e517f /Makefile
parent46f7f0bc4a1cb1a403d414ecec23273a5becd236 (diff)
Achèvement suppression traducteur dans contrib/interface
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 09265105c4..4678b56476 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ NOARG:
@echo "For make to be verbose, add VERBOSE=1"
# build and install the three subsystems: coq, coqide, pcoq
-world: coq coqide # pcoq
+world: coq coqide pcoq
install: install-coq install-coqide install-pcoq
#install-manpages: install-coq-manpages install-pcoq-manpages