diff options
| author | Guillaume Melquiond | 2015-05-14 09:53:36 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-05-14 09:53:36 +0200 |
| commit | 4ad6855504db2ce15a474bd646e19151aa8142e2 (patch) | |
| tree | b72697c8450705186f1337fe9cc9883106dc458d /lib/flags.mli | |
| parent | d91addb140ba7315d70c4599b0d058bef798ac1c (diff) | |
Disable precompilation for native_compute by default.
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 756d3b8515..1f68a88f3a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -128,8 +128,8 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(* Disabling native code compilation for conversion and normalization *) -val no_native_compiler : bool ref +(* Native code compilation for conversion and normalization *) +val native_compiler : bool ref (* Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref |