File indexing completed on 2024-05-19 16:38:22
0001 #!/bin/bash 0002 0003 if [ ! -f "contrib/run-krazy.sh" ]; 0004 then 0005 echo "This script needs to be started from KAMD's root directory" 0006 exit 0007 fi 0008 0009 DIRS=$1 0010 0011 if [ ! -n "$1" ]; 0012 then 0013 DIRS="lib service utils workspace" 0014 fi 0015 0016 0017 0018 echo $DIRS 0019 CURRENT_DIRECTORY=$PWD 0020 0021 for dir in $DIRS; 0022 do 0023 echo "Running krazy2 on $dir ..." 0024 cd $CURRENT_DIRECTORY/src/$dir && krazy2all --exclude license > /tmp/$dir.krazy 0025 done