diff --git a/Scripts/developer_scripts/autotest_cgal b/Scripts/developer_scripts/autotest_cgal index b72e77ae6a9..eee4b1dcbe3 100755 --- a/Scripts/developer_scripts/autotest_cgal +++ b/Scripts/developer_scripts/autotest_cgal @@ -880,8 +880,10 @@ if [ ${?} != 0 ]; then fi fi fi +# Make that file writable (lockfile create read-only files +chmod u+x "$LOCK_FILE" # Put the PID of current process in the lock file -echo $$ >> "$LOCK_FILE" +echo $$ > "$LOCK_FILE" # that line makes the script remove the lock file in case of unwanted exit trap "rm -f $LOCK_FILE" EXIT HUP INT TERM