aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-17 17:38:30 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-17 17:38:30 +0000
commitad4c5a227ba70f01a4970767ccf69a7b79e16a39 (patch)
tree812439160b7ee5275b7b7b7d1855cbb2faecdd46 /config
parent5855215c24e6e0e36faef51ab1d0102170eb7999 (diff)
install de coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5523 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template7
1 files changed, 2 insertions, 5 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index d3f853f17..3970fd738 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -79,17 +79,14 @@ OSDEPLIBS=OSDEPENDENTLIBS
# Win32 systems : .exe
EXE=EXECUTEEXTENSION
-# the command used to install binaries, libs and help files
-INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION
-
# the command MKDIR (try to replace it with mkdirhier if you have problems)
MKDIR=mkdir -p
# where to put the coqdoc.sty style file
-BASETEXDIR=TEXDIRECTORY
+COQDOCDIR=COQDOCDIRECTORY
# command to update TeX' kpathsea database
-MKTEXLSR=MKTEXLSRCOMMAND
+#MKTEXLSR=MKTEXLSRCOMMAND
#the command STRIP
# Unix systems and profiling: true