new shortcuts

[helm.git] / helm / matita / matitaGui.mli

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index cb2cbeb0c00ef46775cb549b4d54b8d62d7d538c..f517bbb9cb3c59415cc6e87933e353af687e3ec5 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -88,6 +88,7 @@ val interactive_uri_choice:
   ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
   ?msg:string -> ?nonvars_button:bool -> 
   ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
+  ?ok_action:[`AUTO|`SELECT] ->
   ?copy_cb:(string -> unit) -> unit ->
     MatitaDisambiguator.choose_uris_callback