]> matita.cs.unibo.it Git - helm.git/commitdiff
* updated for gtk2
authorLuca Padovani <luca.padovani@unito.it>
Wed, 29 Oct 2003 09:59:56 +0000 (09:59 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Wed, 29 Oct 2003 09:59:56 +0000 (09:59 +0000)
helm/gTopLevel/texTermEditor.ml

index 0479388286f8698b93080b883017cb972647b516..c89fe04b2da80a94b53d0d38f4b425b1e040b354 100644 (file)
@@ -126,7 +126,7 @@ module Make(C:Disambiguate.Callbacks) =
           Mathml_editor.drop tex_editor
            (List.mem `CONTROL (GdkEvent.Key.state e))
          else if key = GdkKeysyms._v then
-           ignore (mmlwidget#misc#convert_selection "STRING" `PRIMARY);
+           ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
          let adj = mmlwidget#get_hadjustment in
           mmlwidget#thaw ;
           adj#set_value adj#upper ;