# 
# patch "view.ml"
#  from [214a899619bb1cdc842f53cff5e7a560608e141c]
#    to [e4b963561802c88a3939e9ed4cdb7f1e24776340]
# 
========================================================================
--- view.ml	214a899619bb1cdc842f53cff5e7a560608e141c
+++ view.ml	e4b963561802c88a3939e9ed4cdb7f1e24776340
@@ -143,6 +143,23 @@
 
   let initial_height = 175
 
+  let proper_id_select label ev =
+    if GdkEvent.Button.button ev = 1 && GdkEvent.get_type ev = `TWO_BUTTON_PRESS
+    then begin
+      let txt = label#text in
+      let nl = try String.index txt '\n' with Not_found -> 0 in
+      if string_is_prefix "Revision: " txt
+	  && string_is_prefix "Manifest: " ~offset:(nl+1) txt
+      then begin
+	if label#cursor_position <= nl
+	then label#select_region 10 nl
+	else label#select_region (nl + 1 + 10) (-1) ;
+	true
+      end
+      else false
+    end
+    else false
+
   let make ~packing =
     let pane = GPack.paned `HORIZONTAL ~packing () in
 
@@ -153,6 +170,10 @@
     label#set_selectable true ;
     let empty_label = Printf.sprintf "<tt>%50s</tt>" " " in
     label#set_label empty_label ;
+    ignore (GtkSignal.connect
+	      ~sgn:GtkBase.Widget.Signals.Event.button_press
+	      ~callback:(proper_id_select label)
+	      label#as_widget) ;
 
 
     let rev_columns = new GTree.column_list in