From abea8d06adc8f07aa5d8510c041211b7f4d97c15 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 23 Apr 2020 14:45:06 +0200
Subject: [PATCH] [autocomplete] don't mess with COMPREPLY variable...
---
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 e067d035e17..db940aff16c 100644
--- a/share/autocomplete_frama-c
+++ b/share/autocomplete_frama-c
@@ -94,12 +94,12 @@ _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"
local ambigous="$(bind -v | grep show-all-if-ambiguous)"
ambigous="${ambigous##* }"
if [[ "$ambigous" == "on" ]]
then
COMPREPLY=( $( compgen -W "${advance_options}" -- "${cur##*,}" ) )
- COMPREPLY+=( $( compgen -W "none script tip native:alt-ergo native:coq native:coqide" -- "${cur##*,}" ) )
[[ ${#COMPREPLY[@]} -eq 1 ]] && COMPREPLY=( ${COMPREPLY/#/$prefix} )
else
COMPREPLY=( $( compgen -P "$prefix" -W "${advance_options}" -- "${cur##*,}" ) )
--
GitLab