changeset 2328 | e077dc264dff |
parent 2326 | 16c1b1412b0d |
child 2335 | 366e64ecba91 |
--- a/scripts/build.sh Mon May 18 19:37:38 2009 +0200 +++ b/scripts/build.sh Mon May 18 20:23:42 2009 +0200 @@ -20,6 +20,17 @@ APP_DIRS=${APP_DIRS:-"${DEFAULT_APP_DIRS}"} ZIP_FILES=${ZIP_FILES:-"${DEFAULT_ZIP_FILES}"} + +if [ "$1" != "--skip-pylint" ]; then + cd pylint + bash do_pylint.sh --silent + if [ "$?" != "1" ] ; then + echo ' Build failed. Build script encountered pylint errors.' + exit 1 + fi + cd .. +fi + if [ -e $APP_FOLDER ] ; then cd $APP_FOLDER else