diff options
| author | Prashanth Mundkur | 2018-04-17 16:38:24 -0700 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-04-17 16:38:24 -0700 |
| commit | ac0840873d07b475ce9bdcb0a53ead7e377f1dcd (patch) | |
| tree | 00d869dc074bd8c6ea400c67afcc0233fa301208 /src/value.ml | |
| parent | ffc274b5acbf09051c277ddab0ea4a9e2e1bdc2a (diff) | |
Separate out the trap handler, and make it use the delegatee privilege.
Diffstat (limited to 'src/value.ml')
0 files changed, 0 insertions, 0 deletions