diff options
| author | Maxime Dénès | 2018-02-01 18:37:38 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-01 18:37:38 +0100 |
| commit | 700c08b1215e11470814ce82e04551ffc00cdfeb (patch) | |
| tree | b32e5a44f98296b9e38aa76d8c25ed5fc6283ff8 /engine | |
| parent | 8e3aef19711fa6ccbcb2946afdb690c2fc3d900d (diff) | |
| parent | f1d74986cdd91849c9b86721265c652e1397db02 (diff) | |
Merge PR #6672: [stm] Move options to a per-document record.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions