From 11c52f0882b39afe853473f7a9289e62d1ca843a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 15 Jun 2017 12:36:54 +0200 Subject: [ide] Better exn printing. [fixes BZ#5524] Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies. --- ide/ide_slave.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef..6298d9f09 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -341,6 +341,7 @@ let about () = { } let handle_exn (e, info) = + let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) -- cgit v1.2.3