- some code patched

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1726725c15370b146e42439def72b6b34c23c655..bda4c4b826126a2caf354bfdd5e7838227e6f8d6 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1058,7 +1058,7 @@ module DisambiguateCallbacks =
     interactive_user_uri_choice ~selection_mode ?ok
      ?enable_button_for_non_vars ~title ~msg
   let interactive_interpretation_choice = interactive_interpretation_choice
-  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
+  let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
  end
 ;;