From 4019f7f93ffc05e4ca98bcaafc8a681adff040b6 Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Wed, 29 Oct 2003 09:17:30 +0000 Subject: [PATCH] * variant types changed for selection mode --- helm/gTopLevel/disambiguate.ml | 4 ++-- helm/gTopLevel/disambiguate.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index ce41208dd..974e0b49e 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -46,7 +46,7 @@ module type Callbacks = val output_html : string -> unit val interactive_user_uri_choice : - selection_mode:[`SINGLE | `EXTENDED] -> + selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list @@ -85,7 +85,7 @@ module Make(C:Callbacks) = | [uri] -> [uri] | _ -> C.interactive_user_uri_choice - ~selection_mode:`EXTENDED + ~selection_mode:`MULTIPLE ~ok:"Try every selection." ~enable_button_for_non_vars:true ~title:"Ambiguous input." diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli index 9fdfb8993..0114ce27f 100644 --- a/helm/gTopLevel/disambiguate.mli +++ b/helm/gTopLevel/disambiguate.mli @@ -46,7 +46,7 @@ module type Callbacks = val output_html : string -> unit val interactive_user_uri_choice : - selection_mode:[`SINGLE | `EXTENDED] -> + selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list -- 2.39.2