diff --git a/Scripts/developer_scripts/autotest_cgal b/Scripts/developer_scripts/autotest_cgal index e091a413d44..898683124ac 100755 --- a/Scripts/developer_scripts/autotest_cgal +++ b/Scripts/developer_scripts/autotest_cgal @@ -232,8 +232,8 @@ test_script() else MAKE_OPTS="-j ${NUMBER_OF_PROCESSORS}" fi - - cat > ${TEST_DIR_ROOT}/localtestscript.${1} < ${CGAL_TEST_DIR}/localtestscript.${1} <> ${ACTUAL_LOGFILE}.${1} 2>&1 + chmod ugo+x ${CGAL_TEST_DIR}/localtestscript.${1} + remote_command ${1} "${CGAL_TEST_DIR}/localtestscript.${1}" >> ${ACTUAL_LOGFILE}.${1} 2>&1 log_done ${ACTUAL_LOGFILE}.${1} #PLATFORM=`basename $CGAL_MAKEFILE | sed -e "s/makefile_//g"` #