# 
# patch "ui.ml"
#  from [2ab3b05377540a6ddfc6d893d74691e495c1ee58]
#    to [3c6f04a0d57dbed565e1305c6cdab1c8c6db2253]
# 
========================================================================
--- ui.ml	2ab3b05377540a6ddfc6d893d74691e495c1ee58
+++ ui.ml	3c6f04a0d57dbed565e1305c6cdab1c8c6db2253
@@ -46,7 +46,8 @@
     mutable popup_id : string ;
     group           : GAction.action_group ;
     mutable signals : (unit Gobject.obj * GtkSignal.id) list ;
-    clipboard       : GData.clipboard ;
+    clipboard1       : GData.clipboard ;
+    clipboard2       : GData.clipboard ;
   }
 
 type manager = {
@@ -94,7 +95,8 @@
     group      = g ;
     signals    = [] ;
     popup_id   = "" ;
-    clipboard  = GData.clipboard Gdk.Atom.clipboard
+    clipboard1  = GData.clipboard Gdk.Atom.clipboard ;
+    clipboard2  = GData.clipboard Gdk.Atom.primary
   }
 
 let make_manager () =
@@ -132,10 +134,12 @@
     let data = Database.fetch_revision (some v.View.db) popup_id in
     remember_signal copy_revision
       (fun () ->
-	p.clipboard#set_text data.revision_id) ;
+	p.clipboard1#set_text data.revision_id ;
+	p.clipboard2#set_text data.revision_id) ;
     remember_signal copy_manifest
       (fun () ->
-	p.clipboard#set_text data.manifest_id)
+	p.clipboard1#set_text data.manifest_id ;
+	p.clipboard2#set_text data.manifest_id)
   end ;
 
   (* Setup the "diff with other entry" *)