diff options
Diffstat (limited to 'config/Makefile.template')
| -rw-r--r-- | config/Makefile.template | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index 4e592e6e6..5310aec94 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -102,7 +102,7 @@ EXE=EXECUTEEXTENSION MKDIR=mkdir -p # where to put the coqdoc.sty style file -COQDOCDIR=COQDOCDIRECTORY +COQDOCDIR="COQDOCDIRECTORY" # command to update TeX' kpathsea database #MKTEXLSR=MKTEXLSRCOMMAND |