diff --git a/make_help_scripts/add_review_stats b/make_help_scripts/add_review_stats old mode 100644 new mode 100755 diff --git a/make_help_scripts/deploy_defines b/make_help_scripts/deploy_defines index 1ddebc38ccb..12ee0690059 100755 --- a/make_help_scripts/deploy_defines +++ b/make_help_scripts/deploy_defines @@ -12,13 +12,14 @@ build_dir="_build" # reviewer stats reviewer_stats_filename="reviewers_stats_with_graph.html" -reviewer_stats_cache_folder="~/reviews" +reviewer_stats_cache_folder="reviews" reviewer_stats_target_folder="./doc/acknowledgements" add_reviewer_stats_file () { - if [[ -f "${reviewer_stats_cache_folder}/${reviewer_stats_filename}" ]]; then + ORIGFILE="$HOME/$reviewer_stats_cache_folder/$reviewer_stats_filename" + if test -f "$ORIGFILE"; then echo "Copy reviewer stats file to ${reviewer_stats_target_folder}" - cp ${reviewer_stats_cache_folder}/${reviewer_stats_filename} ${reviewer_stats_target_folder} + cp ${ORIGFILE} ${reviewer_stats_target_folder} else echo "Create empty reviewer stats file in ${reviewer_stats_target_folder}" touch ${reviewer_stats_target_folder}/${reviewer_stats_filename}