aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-05-07 15:53:21 +0200
committerGaëtan Gilbert2020-05-07 15:53:21 +0200
commit17e7aeef98ca8c341fae05d5e94b50b4ee7687f6 (patch)
tree3f1917332a46d302e62bc3f1a97f21b9e80da211
parent06b1672e4d4390aad693812321693b3cd5ee668a (diff)
parent14ada0952a362968be1bfc2085ad1a233372e7ab (diff)
Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)
Reviewed-by: SkySkimmer
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index cf9141853d..3140df4cee 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -249,8 +249,8 @@ MLINCLUDES=$(LOCALINCLUDES)
USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS))
-OCAMLC := $(TIMER) $(OCAMLFIND) ocamlc $(CAMLFLAGS)
-OCAMLOPT := $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS)
+OCAMLC = $(TIMER) $(OCAMLFIND) ocamlc $(CAMLFLAGS)
+OCAMLOPT = $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS)
BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)