From 89f5d25c2f7c919ebf581fad78d4ba39992e4007 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 23 Oct 2018 14:38:01 +0200
Subject: Fix issue #8801.

When opening the query pane, do not try to focus on a query tab that no
longer exists.
---
 ide/wg_Command.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 8eddfb3149..740ab9c873 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -152,9 +152,9 @@ object(self)
   method show =
     frame#show;
     let cur_page = notebook#get_nth_page notebook#current_page in
-    let _, _, e =
-      List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in
-    e#misc#grab_focus ()
+    match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with
+    | (_, _, e) -> e#misc#grab_focus ()
+    | exception Not_found -> ()
 
   method hide =
     frame#hide
-- 
cgit v1.2.3