diff options
| author | Guillaume Melquiond | 2016-09-30 21:11:02 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-10-01 07:50:12 +0200 |
| commit | 5b6dd304b9f88c86ebb066c1f173bb011d2b5f83 (patch) | |
| tree | b1f30879412871ef7fdad8f23fc5de4e1dd0d0c8 /kernel/nativecode.ml | |
| parent | 064de6f6839c4ef963b83018812c5d4113eb2bb9 (diff) | |
Allow appending to string options.
Whether an option should be set or appended to is stored as a 2-value
flag next to the new content. This commit also cleans the code by
declaring a single object for each persistent option rather than three
different ones (one per locality).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions