diff options
| author | Emilio Jesus Gallego Arias | 2018-01-31 05:38:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-01-31 07:50:45 +0100 |
| commit | f1d74986cdd91849c9b86721265c652e1397db02 (patch) | |
| tree | a8a28085a757db5c1b303523bf48dc298c73680c /dev/ci/ci-basic-overlay.sh | |
| 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 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions