diff options
Diffstat (limited to 'lib/loc.ml')
| -rw-r--r-- | lib/loc.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index 8f133ce0d..5ca345fd2 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -74,4 +74,6 @@ let add_loc e loc = Exninfo.add e location loc let get_loc e = Exninfo.get e location -let raise loc e = raise (Exninfo.add e location loc) +let raise loc e = + let info = Exninfo.add Exninfo.null location loc in + Exninfo.iraise (e, info) |