PR all and cleanup

leanprover-community · Aug 2, 2024 · 1ee940e · 1ee940e
1 parent 6fa92da
commit 1ee940e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 44 deletions.
diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml
@@ -58,46 +58,4 @@ jobs:
               s=\n---\nReports\n\n=\n</details>\n\n---\n\n<details><summary>Reports</summary>\n\n=
               s=\n---[\n]*$=\n\n</details>\n&=
             ')"
-          sed -i "s=\${GITHUB_REPOSITORY}=leanprover-community/blog=" mathlib/scripts/update_PR_comment.sh
-          chmod u+rx mathlib/scripts/update_PR_comment.sh
-          cat mathlib/scripts/update_PR_comment.sh
-
-          # the text of the message that will replace the current one
-          message="${mim}"
-          # the start of the message to locate it among all messages in the PR
-          comment_init="${title}"
-          # the PR number
-          #PR="${PR}"
-          echo "using: '${title}' '${PR}'"
-          data=$(jq -n --arg msg "hello" '{"body": $msg}') # "$message" '{"body": $msg}')
-          echo "data: ${data}"
-          #man jq
-          baseURL="https://api.github.com/repos/leanprover-community/blog/issues"
-          printf 'Base url: %s\n' "${baseURL}"
-          method="POST"
           printf '%s\n' "${mim}" > "${GITHUB_STEP_SUMMARY}"
-          #./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-          if [[ -n "$message" ]]; then
-              url="${baseURL}/${PR}/comments"
-              printf 'Base url: %s\n' "${url}"
-              headers="Authorization: token ${GITHUB_TOKEN}"
-              comment_id=$(curl -s -S -H "Content-Type: application/json" -H "$headers" "$url" |
-                jq --arg cID "${comment_init}" -r '.[] | select(.body | startswith($cID)) | .id' | head -1)
-              echo "Comment id: '${comment_id}'"
-              if [[ -n "$comment_id" ]]; then
-                  url="${baseURL}/comments/${comment_id}"
-                  echo "are we here?"
-                  method="PATCH"
-              fi
-              echo "or are we there?"
-              curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url"
-          fi
-
-          #echo "running script"
-          #./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" &&
-          #  echo "after script"
-          #name: print_lost_declarations
-          #run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          #git checkout -q master
-          #git checkout -q -
diff --git a/monthly_summary.sh b/monthly_summary.sh
@@ -78,8 +78,8 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}"   | sed -z 's=^\[=='
     }
   '
 
-only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=  =' | tr -d '()')"
-only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=  =' | tr -d '()')"
+only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')"
+only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')"
 
 printf $'\n---\nReports\n\n'