diff options
| author | Kathy Gray | 2015-06-09 16:04:54 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-06-09 16:04:54 +0100 |
| commit | 645839c91e257e4ed30cca34dc49391b5bbfb591 (patch) | |
| tree | 7462cebada7bd1f30d28da2f66b3f06f9a0de85e /src/util.ml | |
| parent | bfbf5125780181fd41fd74986a4dd1654f35be48 (diff) | |
support exit/escape out of the interface
Diffstat (limited to 'src/util.ml')
0 files changed, 0 insertions, 0 deletions