aboutsummaryrefslogtreecommitdiffhomepage
path: root/config/Makefile.template
diff options
context:
space:
mode:
Diffstat (limited to 'config/Makefile.template')
-rw-r--r--config/Makefile.template6
1 files changed, 6 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 0749c3540..d3f853f17 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -85,6 +85,12 @@ 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
+
+# command to update TeX' kpathsea database
+MKTEXLSR=MKTEXLSRCOMMAND
+
#the command STRIP
# Unix systems and profiling: true
# Unix systems and no profiling: strip