diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/Makefile.template | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index 67c4c34d1..409e49467 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -30,6 +30,7 @@ LOCAL=LOCALINSTALLATION BINDIR="BINDIRDIRECTORY" COQLIB="COQLIBDIRECTORY" MANDIR="MANDIRDIRECTORY" +DOCDIR="DOCDIRDIRECTORY" EMACSLIB="EMACSLIBDIRECTORY" EMACS=EMACSCOMMAND |