diff options
| author | Gaëtan Gilbert | 2020-05-07 15:53:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-07 15:53:21 +0200 |
| commit | 17e7aeef98ca8c341fae05d5e94b50b4ee7687f6 (patch) | |
| tree | 3f1917332a46d302e62bc3f1a97f21b9e80da211 | |
| parent | 06b1672e4d4390aad693812321693b3cd5ee668a (diff) | |
| parent | 14ada0952a362968be1bfc2085ad1a233372e7ab (diff) | |
Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)
Reviewed-by: SkySkimmer
| -rw-r--r-- | Makefile.build | 4 |
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) |
