scripts/addToolVersion.sh
changeset 1872 d7787259005e
parent 1852 3f6a165d8ba7
child 1920 6df2d4f78948
     1.1 --- a/scripts/addToolVersion.sh	Sat Mar 20 18:49:15 2010 +0100
     1.2 +++ b/scripts/addToolVersion.sh	Mon Mar 29 23:37:29 2010 +0200
     1.3 @@ -158,12 +158,12 @@
     1.4          --duma)     EXP=; OBS=; cat=DUMA;           tool=duma;      tool_prefix=debug;;
     1.5          --strace)   EXP=; OBS=; cat=STRACE;         tool=strace;    tool_prefix=debug;;
     1.6          --ltrace)   EXP=; OBS=; cat=LTRACE;         tool=ltrace;    tool_prefix=debug;;
     1.7 -        --libelf)   EXP=; OBS=; cat=LIBELF;         tool=libelf;    tool_prefix=tools;;
     1.8          --gmp)      EXP=; OBS=; cat=GMP;            tool=gmp;       tool_prefix=companion_libs;;
     1.9          --mpfr)     EXP=; OBS=; cat=MPFR;           tool=mpfr;      tool_prefix=companion_libs;;
    1.10          --ppl)      EXP=; OBS=; cat=PPL;            tool=ppl;       tool_prefix=companion_libs;;
    1.11          --cloog)    EXP=; OBS=; cat=CLOOG;          tool=cloog;     tool_prefix=companion_libs;;
    1.12          --mpc)      EXP=; OBS=; cat=MPC;            tool=mpc;       tool_prefix=companion_libs;;
    1.13 +        --libelf)   EXP=; OBS=; cat=LIBELF;         tool=libelf;    tool_prefix=companion_libs;;
    1.14  
    1.15          # Tools options:
    1.16          -x|--experimental|+s)   EXP=1;;