aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authornotin2008-06-12 13:07:09 +0000
committernotin2008-06-12 13:07:09 +0000
commit6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb (patch)
tree782ae680f457e7acd9111eff328ee2cd725a5eec /Makefile.common
parent7a337e554e21f2943fa37f6ecee09e3b52be7772 (diff)
Remplacement des 'cp' et 'mkdir' par 'install'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index 7719572f02..3ba85f9a49 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,6 +29,10 @@ CHICKENOPT:=bin/coqchk.opt$(EXE)
BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
CHICKEN:=bin/coqchk$(EXE)
+INSTALLBIN:=install
+INSTALLLIB:=install -m 644
+MKDIR:=install -d
+
COQIDEBYTE:=bin/coqide.byte$(EXE)
COQIDEOPT:=bin/coqide.opt$(EXE)
COQIDE:=bin/coqide$(EXE)