diff -r 5416f4ba36bf -r 48c12c696778 scripts/addToolVersion.sh
--- a/scripts/addToolVersion.sh	Sun May 03 21:10:15 2009 +0000
+++ b/scripts/addToolVersion.sh	Tue May 05 22:04:20 2009 +0000
@@ -13,7 +13,7 @@
   'tool' in one of:
     --gcc, --binutils, --glibc, --eglibc, --uClibc, --linux,
     --gdb, --dmalloc, --duma, --strace, --ltrace, --libelf
-    --gmp, --mpfr
+    --gmp, --mpfr, --ppl
 
   Valid options for all tools:
     --stable, -s, +x   (default)
@@ -133,6 +133,7 @@
         --libelf)   EXP=; OBS=; cat=LIBELF;    tool=libelf;   tool_prefix=tools;;
         --gmp)      EXP=; OBS=; cat=GMP;       tool=gmp;      tool_prefix=companion_libs;;
         --mpfr)     EXP=; OBS=; cat=MPFR;      tool=mpfr;     tool_prefix=companion_libs;;
+        --ppl)      EXP=; OBS=; cat=PPL;       tool=ppl;      tool_prefix=companion_libs;;
 
         # Tools options:
         -x|--experimental|+s)   EXP=1;;