aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template3
1 files changed, 3 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 3970fd738..cd49db893 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -37,6 +37,9 @@ VERSION=COQVERSION
# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
CAMLP4BIN=CAMLP4BINDIRECTORY
+# Ocaml version number
+CAMLVERSION=CAMLTAG
+
# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
CAMLP4O=CAMLP4TOOL
MYCAMLP4LIB=CAMLP4LIBDIRECTORY