diff options
| author | Gabriel Kerneis | 2013-10-15 16:02:22 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2013-10-15 16:02:22 +0100 |
| commit | be581b5752f089b1f530e14d0a189b787b268e96 (patch) | |
| tree | c1c17d7754879c982316459aa978cc9b50bdbbb4 /src/reporting_basic.mli | |
| parent | b5bcb90619b75213fb8a8a2f64017937e8572aea (diff) | |
Resume interpreter after actions
At the moment, writes are ignored and reads always return unit.
Diffstat (limited to 'src/reporting_basic.mli')
0 files changed, 0 insertions, 0 deletions