The disambiguation now returns a list of interpretations.

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9ff7e8fc6cc13a386c41ee316103150abaeb6fae..5df73dc1cacbc71b3fb61443838829c32582888c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -379,7 +379,7 @@ let interactive_interpretation_choice interpretations =
  GtkThread.main ();
  match !chosen with
     None -> raise NoChoice
-  | Some n -> n
+  | Some n -> [n]
 ;;