diff --git a/Scripts/developer_scripts/autotest_cgal b/Scripts/developer_scripts/autotest_cgal index 09c6f59167c..8c919c9a374 100755 --- a/Scripts/developer_scripts/autotest_cgal +++ b/Scripts/developer_scripts/autotest_cgal @@ -893,6 +893,8 @@ else MAKE_CMD='make' fi +if [ -z "$IS_CYGWIN" ]; then + # Acquire lock lockfile -r 1 "$LOCK_FILE"; if [ ${?} != 0 ]; then @@ -915,6 +917,8 @@ chmod u+w "$LOCK_FILE" # Put the PID of current process in the lock file echo $$ > "$LOCK_FILE" +fi + # that line makes the script remove the lock file in case of unwanted exit trap "rm -f \"$LOCK_FILE\"" EXIT HUP INT TERM