From 8f4d0165f0a1be1b81ecab0356f7040423406c28 Mon Sep 17 00:00:00 2001
From: vgross
Date: Mon, 7 Dec 2009 15:35:35 +0000
Subject: Remove the "detach script windows" feature.

See bug #2173.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12567 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 25 -------------------------
 1 file changed, 25 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 734bdccdc0..99b2593087 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3113,31 +3113,6 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 							   !current.show_toolbar <- not !current.show_toolbar;
 							   !show_toolbar !current.show_toolbar)
 					  in
-					  let _ = configuration_factory#add_item
-					    "Detach _Script Window"
-					    ~callback:
-					    (do_if_not_computing "detach script window" (sync
-											   (fun () ->
-											      let nb = session_notebook in
-												if nb#misc#toplevel#get_oid=w#coerce#get_oid then
-												  begin
-												    let nw = GWindow.window
-												      ~width:(!current.window_width*2/3)
-												      ~height:(!current.window_height*2/3)
-												      ~position:`CENTER
-												      ~wm_name:"CoqIde"
-												      ~wm_class:"CoqIde"
-												      ~title:"Script"
-												      ~show:true () in
-												    let parent = Option.get nb#misc#parent in
-												      ignore (nw#connect#destroy
-														~callback:
-														(fun () -> nb#misc#reparent parent));
-												      nw#add_accel_group accel_group;
-												      nb#misc#reparent nw#coerce
-												  end
-											   )))
-					  in
 					  let _ =
 					    configuration_factory#add_item
 					      "Detach _View"
-- 
cgit v1.2.3