IDE: suppressed compilation warning

29051ec3 · MARCHE Claude · 3cffb857 · 29051ec3
Commit 29051ec3 authored Feb 05, 2016 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

src/ide/gmain.ml src/ide/gmain.ml +1 -1

No files found.
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -2070,7 +2070,7 @@ let reload () =
    | e ->
        begin
          match e with
-          | Loc.Located(loc,e) ->
+          | Loc.Located(loc,_) ->
            scroll_to_loc ~color:error_tag ~yalign:0.5 loc;
            notebook#goto_page source_page (* go to "source" tab *)
          | _ -> ()