aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template6
1 files changed, 5 insertions, 1 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index d5c2a1436..1907cb0d6 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -51,11 +51,15 @@ MYCAMLP4LIB=CAMLP4LIBDIRECTORY
# Objective-Caml compile command
OCAMLC=BYTECAMLC
OCAMLOPT=NATIVECAMLC
+OCAMLDEP=OCAMLDEPEXEC
+OCAMLDOC=OCAMLDOCEXEC
+OCAMLLEX=OCAMLLEXEXEC
+OCAMLYACC=OCAMLYACCEXEC
# Caml link command and Caml make top command
CAMLLINK=BYTECAMLC
CAMLOPTLINK=NATIVECAMLC
-CAMLMKTOP=ocamlmktop
+CAMLMKTOP=CAMLMKTOPEXEC
# Compilation debug flag
CAMLDEBUG=COQDEBUGFLAG