aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorglondu2008-08-16 21:16:05 +0000
committerglondu2008-08-16 21:16:05 +0000
commit22739b29af99bc06c1d63003853650df5de47f8f (patch)
tree4a75d36747473c6456d16de3edec310b93291874 /Makefile.common
parenta3f08185150e8ae0ce00e142edfcf7009f126e93 (diff)
Install csdpcert with libraries
csdpcert is not meant to be called directly by the user git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 6b7da1a57c..3aacdef732 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -46,7 +46,7 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
endif
OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
-CSDPCERT:=bin/csdpcert$(EXE)
+CSDPCERT:=contrib/micromega/csdpcert$(EXE)
###########################################################################
# tools