From 490fcaab846dc926c0945df6b0f8fb18c5bb0dd9 Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 16 Apr 2007 12:06:35 +0000
Subject: Fix a bug which sometimes made coqide crash after changing
 preferences (first fixed in rev. 9716).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/utils/configwin_ihm.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'ide/utils')

diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index e9ba9789bd..240fd829d8 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1108,10 +1108,6 @@ let edit ?(with_apply=true)
       List.iter (fun param_box -> param_box#apply) list_param_box  ;
       apply ()
     in
-    let f_ok () =
-      List.iter (fun param_box -> param_box#apply) list_param_box  ;
-      Return_ok
-    in
     let destroy () =
       tooltips#destroy () ;
       dialog#destroy ();
@@ -1120,7 +1116,7 @@ let edit ?(with_apply=true)
       try
 	match dialog#run () with
 	  | `APPLY  -> f_apply (); iter Return_apply
-	  | `OK -> destroy (); f_ok ()
+	  | `OK -> f_apply (); destroy (); Return_ok
 	  | _ -> destroy (); rep
       with
 	  Failure s ->
-- 
cgit v1.2.3