ExternalProject: Retry on a failed git clone

Git sometimes fails to clone repositories due to network outage or
server load.  Try 3 times before giving up.
This commit is contained in:
Bill Hoffman 2013-03-20 17:54:49 -04:00 committed by Brad King
parent 2557e84d67
commit 118f741c49
1 changed files with 15 additions and 5 deletions

View File

@ -287,11 +287,21 @@ if(error_code)
message(FATAL_ERROR \"Failed to remove directory: '${source_dir}'\") message(FATAL_ERROR \"Failed to remove directory: '${source_dir}'\")
endif() endif()
execute_process( # try the clone 3 times incase there is an odd git clone issue
set(error_code 1)
set(number_of_tries 0)
while(error_code AND number_of_tries LESS 3)
execute_process(
COMMAND \"${git_EXECUTABLE}\" clone \"${git_repository}\" \"${src_name}\" COMMAND \"${git_EXECUTABLE}\" clone \"${git_repository}\" \"${src_name}\"
WORKING_DIRECTORY \"${work_dir}\" WORKING_DIRECTORY \"${work_dir}\"
RESULT_VARIABLE error_code RESULT_VARIABLE error_code
) )
math(EXPR number_of_tries \"\${number_of_tries} + 1\")
endwhile()
if(number_of_tries GREATER 1)
message(STATUS \"Had to git clone more than once:
\${number_of_tries} times.\")
endif()
if(error_code) if(error_code)
message(FATAL_ERROR \"Failed to clone repository: '${git_repository}'\") message(FATAL_ERROR \"Failed to clone repository: '${git_repository}'\")
endif() endif()