diff --git a/resources/printResourceInformation.sh b/resources/printResourceInformation.sh index e54fd707..4e0270c6 100644 --- a/resources/printResourceInformation.sh +++ b/resources/printResourceInformation.sh @@ -1,9 +1,18 @@ #!/bin/bash +if [ "$HEIDELTIME_HOME" = "" ] ; then + echo "please set \$HEIDELTIME_HOME" + exit -1 +fi + +PWD=$(pwd) +cd $HEIDELTIME_HOME/resources + echo "Writing used_resources.txt" find ./ -name "*.txt" > used_resources.txt echo "Copying resources..." -cp -r * ../class/ +cp -r $HEIDELTIME_HOME/resources/* $HEIDELTIME_HOME/class/ echo "done." +cd $PWD