diff options
Diffstat (limited to 'scripts/addToolVersion.sh')
| -rwxr-xr-x | scripts/addToolVersion.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scripts/addToolVersion.sh b/scripts/addToolVersion.sh index 0f6bf034..21f4e9e0 100755 --- a/scripts/addToolVersion.sh +++ b/scripts/addToolVersion.sh @@ -131,8 +131,8 @@ while [ $# -gt 0 ]; do --strace) EXP=; OBS=; cat=STRACE; tool=strace; tool_prefix=debug;; --ltrace) EXP=; OBS=; cat=LTRACE; tool=ltrace; tool_prefix=debug;; --libelf) EXP=; OBS=; cat=LIBELF; tool=libelf; tool_prefix=tools;; - --gmp) EXP=; OBS=; cat=GMP; tool=gmp; tool_prefix=gmp_mpfr;; - --mpfr) EXP=; OBS=; cat=MPFR; tool=mpfr; tool_prefix=gmp_mpfr;; + --gmp) EXP=; OBS=; cat=GMP; tool=gmp; tool_prefix=companion_libs;; + --mpfr) EXP=; OBS=; cat=MPFR; tool=mpfr; tool_prefix=companion_libs;; # Tools options: -x|--experimental|+s) EXP=1;; |