diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/Makefile.template | 7 |
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 |