aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Find.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-25 18:11:22 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-25 18:11:22 +0000
commite754b5fcdceb96466905d5b02f682a7e69db15f7 (patch)
treeb51f10ee4c3ccbded47d5e64546915d498c65b89 /ide/wg_Find.ml
parent96afc7389d45ce85255982058e4688c71266a700 (diff)
Fixup last commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16144 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Find.ml')
-rw-r--r--ide/wg_Find.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 83d1a1a23..7dc4adfea 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -222,7 +222,6 @@ class finder (view : GText.view) =
let find_cb ev =
let ev_key = GdkEvent.Key.keyval ev in
let (key, _) = GtkData.AccelGroup.parse "Return" in
- let () = Printf.printf "%i %i\n%!" ev_key key in
if ev_key = key then (self#find_forward (); true)
else false
in