diff --git a/share/autocomplete_frama-c b/share/autocomplete_frama-c index 1b4610d4d3356beddb56c4000185810a4f5aa223..423c17506bf553560fc19a589a1132391a277883 100644 --- a/share/autocomplete_frama-c +++ b/share/autocomplete_frama-c @@ -94,7 +94,7 @@ _frama-c () then local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*}," advance_options="$(frama-c -wp-detect | grep -E -o " \[.*" | grep -E -o "[^][|]*")" - advance_options+="none script tip native:alt-ergo native:coq native:coqide" + advance_options+=" none script tip native:alt-ergo native:coq native:coqide" local ambigous="$(bind -v | grep show-all-if-ambiguous)" ambigous="${ambigous##* }" if [[ "$ambigous" == "on" ]]