From 1ee940e5ff2d4251ec3bf16c6251fcc254f2131a Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Fri, 2 Aug 2024 15:23:29 +0200
Subject: [PATCH] PR all and cleanup

---
 .github/workflows/monthly_pr_report.yaml | 42 ------------------------
 monthly_summary.sh                       |  4 +--
 2 files changed, 2 insertions(+), 44 deletions(-)

diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml
index 9db821c6..bac5b097 100644
--- 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
index 92cb69a5..d67670d5 100755
--- 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'