aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/toplevel.ml')
-rw-r--r--toplevel/toplevel.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index fbdc96d6e..aba5aeb27 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -103,7 +103,7 @@ let get_bols_of_loc ibuf (bp,ep) =
lines_rec ll nafter fl
in
let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in
- (fl,out_some ll)
+ (fl,Option.get ll)
let dotted_location (b,e) =
if e-b < 3 then