Fix ./configure --disable-instrumented-runtime never disabling the instrumented runtime#11611
Conversation
…strumented runtime
0e5af24 to
257dff1
Compare
|
Nice catch! Slightly "simpler" would be to revert the mistake from 78463a7 which incorrectly changed |
|
@Engil do you have a preference whether it should be enabled or disabled by default? If everyone is fine disabling it by default i'll change the PR |
|
The instrumented runtime is enabled by default in 4.14 - not sure that should change (especially as it’s then mildly tricky to rebuild the compiler with it in opam) |
Indeed, that shouldn't be changed in a bugfix branch. |
Octachron
left a comment
There was a problem hiding this comment.
A agree with the simplified fix.
Calling the configure script with
--disable-instrumented-runtimewould never actually disable the instrumented runtime.This should also be backported to the
5.0branch.