diff options
| author | barras | 2005-11-23 17:21:53 +0000 |
|---|---|---|
| committer | barras | 2005-11-23 17:21:53 +0000 |
| commit | e280c8edf8d49f50b9022e20f0ac5f104f123c67 (patch) | |
| tree | b16dd5101ac38a6b25264a794377d3a14069fb6b /ide/undo.ml | |
| parent | fd9eb182a5a45d04c634ea17e2225dddbf667033 (diff) | |
bug de coqide sous windows (bad file descriptor)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/undo.ml')
| -rw-r--r-- | ide/undo.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/ide/undo.ml b/ide/undo.ml index 7a62cd558b..d2fe81e1df 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -18,7 +18,7 @@ let neg act = match act with | Insert (s,i,l) -> Delete (s,i,l) | Delete (s,i,l) -> Insert (s,i,l) -class undoable_view (tv:([> Gtk.text_view ] as 'a) Gtk.obj) = +class undoable_view (tv:[>Gtk.text_view] Gtk.obj) = let undo_lock = ref true in object(self) inherit GText.view tv as super @@ -71,7 +71,6 @@ object(self) (self#buffer#insert_interactive ~iter s) or (Stack.push act history; false) in if r then begin - process_pending (); let act = Stack.pop history in Queue.push act redo; Stack.push act nredo |