From 3ea180f0b3272bbbc4b1feced021627b7ed9c52b Mon Sep 17 00:00:00 2001
From: Lionel Blatter <Lionel.BLATTER@cea.fr>
Date: Fri, 24 Apr 2020 14:00:56 +0200
Subject: [PATCH] [autocomplete] Adding a space to separate options
---
share/autocomplete_frama-c | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/autocomplete_frama-c b/share/autocomplete_frama-c
index 1b4610d4d33..423c17506bf 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" ]]
--
GitLab