scripts/addToolVersion.sh
changeset 1318 5416f4ba36bf
parent 1225 4b065e7e2130
child 1324 48c12c696778
     1.1 --- a/scripts/addToolVersion.sh	Wed Mar 04 17:59:35 2009 +0000
     1.2 +++ b/scripts/addToolVersion.sh	Sun May 03 21:10:15 2009 +0000
     1.3 @@ -131,8 +131,8 @@
     1.4          --strace)   EXP=; OBS=; cat=STRACE;    tool=strace;   tool_prefix=debug;;
     1.5          --ltrace)   EXP=; OBS=; cat=LTRACE;    tool=ltrace;   tool_prefix=debug;;
     1.6          --libelf)   EXP=; OBS=; cat=LIBELF;    tool=libelf;   tool_prefix=tools;;
     1.7 -        --gmp)      EXP=; OBS=; cat=GMP;       tool=gmp;      tool_prefix=gmp_mpfr;;
     1.8 -        --mpfr)     EXP=; OBS=; cat=MPFR;      tool=mpfr;     tool_prefix=gmp_mpfr;;
     1.9 +        --gmp)      EXP=; OBS=; cat=GMP;       tool=gmp;      tool_prefix=companion_libs;;
    1.10 +        --mpfr)     EXP=; OBS=; cat=MPFR;      tool=mpfr;     tool_prefix=companion_libs;;
    1.11  
    1.12          # Tools options:
    1.13          -x|--experimental|+s)   EXP=1;;