diff options
| author | Enrico Tassi | 2013-11-27 17:51:49 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-11-27 17:51:49 +0100 |
| commit | 2923b9262e3859f2ad0169778d63d79843d7ddf7 (patch) | |
| tree | 01ba2bb8f25b984903e5b714d88b48d1e0914296 /lib/interface.mli | |
| parent | 03f268c1c4a872ec37a0995174c305c172339f53 (diff) | |
Old message Interp returns the state id so that one can BackTo it
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 24f2b65249..a01ec20aed 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -236,7 +236,7 @@ type handle_exn_rty = state_id * location * string (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string (* spiwack: [Inl] for safe and [Inr] for unsafe. *) -type interp_rty = (string,string) Util.union +type interp_rty = state_id * (string,string) Util.union type handler = { |