diff options
| author | Emilio Jesus Gallego Arias | 2017-10-11 11:27:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-11 11:27:15 +0200 |
| commit | 16dec9697b06a7fbda0997ab0685ef24443c7d3a (patch) | |
| tree | 1f85ee8f06535198d402ef9879883f3225291e6b /lib/flags.ml | |
| parent | 35c36f80dcc1e61e3dae8bcce1da71b384904582 (diff) | |
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index a178eb7552..a53a866aba 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -42,7 +42,6 @@ let with_extra_values o l f x = Exninfo.iraise reraise let boot = ref false -let load_init = ref true let record_aux_file = ref false |