aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2022-01-05 15:22:22 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2022-01-05 15:22:22 +0100
commit1c264a258be01623b8936657a32f2251ca2059c1 (patch)
treea6c707ef97373ca91b0f476fd3b9ab1ee47fb073 /configure
parent89562c917e61c56a167ba13b86021b286cb7e257 (diff)
downloadcompcert-kvx-1c264a258be01623b8936657a32f2251ca2059c1.tar.gz
compcert-kvx-1c264a258be01623b8936657a32f2251ca2059c1.zip
ccomp profiling
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure1
1 files changed, 1 insertions, 0 deletions
diff --git a/configure b/configure
index 3da00fb3..e21c2424 100755
--- a/configure
+++ b/configure
@@ -661,6 +661,7 @@ SHAREDIR=$sharedir
COQDEVDIR=$coqdevdir
OCAML_NATIVE_COMP=$ocaml_native_comp
OCAML_OPT_COMP=$ocaml_opt_comp
+OCAML_LM_PROF=false
MENHIR_DIR=$menhir_dir
COMPFLAGS=-bin-annot
EOF