File indexing completed on 2023-05-30 12:37:56 

0001 #!/bin/bash
0002 if test ! -f "${BASH_SOURCE[0]}"
0003 then
0004   echo "Error getting the script name"
0005   return
0006   exit
0007 fi
0008 
0009 pathadd () {
0010   if ! echo "$PATH" | grep -Eq "(^|:)$1($|:)"
0011   then
0012     PATH="$PATH:$1"
0013   fi
0014 }
0015 
0016 cd `dirname "${BASH_SOURCE[0]}"`"/bin/"
0017 pathadd `pwd`
0018 cd $OLDPWD