Skip to content
Snippets Groups Projects
Commit 3ea180f0 authored by Lionel Blatter's avatar Lionel Blatter
Browse files

[autocomplete] Adding a space to separate options

parent b4d9934f
No related branches found
No related tags found
No related merge requests found
......@@ -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" ]]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment