diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-31 05:38:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-31 07:50:45 +0100 |
| commit | f1d74986cdd91849c9b86721265c652e1397db02 (patch) | |
| tree | a8a28085a757db5c1b303523bf48dc298c73680c /ide/minilib.ml | |
| parent | c658141acff6d1b7f610960dd39998385c7e8806 (diff) | |
[stm] Move options to a per-document record.
We gather (almost) all the STM options in a record, now set at
document creation time.
This is refactoring is convenient for some other ongoing
functionalization work.
Diffstat (limited to 'ide/minilib.ml')
0 files changed, 0 insertions, 0 deletions