aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 409e49467..f35af2b58 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -56,6 +56,7 @@ MYCAMLP4LIB="CAMLP4LIBDIRECTORY"
COQIDEINCLUDES=LABLGTKINCLUDES
# Objective-Caml compile command
+OCAML="OCAMLEXEC"
OCAMLC="BYTECAMLC"
OCAMLOPT="NATIVECAMLC"
OCAMLDEP="OCAMLDEPEXEC"