summary

.github/workflows/monthly_pr_report.yaml

@@ -23,17 +23,6 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
-      - uses: actions/github-script@v6
-        with:
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            github.rest.issues.createComment({
-              issue_number: context.issue.number,
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              body: '👋 Thanks for reporting!'
-            })
-
       - uses: actions/checkout@v4
         with:
           path: blog
@@ -86,6 +75,8 @@ jobs:
           baseURL="https://api.github.com/repos/leanprover-community/blog/issues"
           printf 'Base url: %s\n' "${baseURL}"
           method="POST"
+          printf '###  Summary\n\n' > "${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}"
@@ -105,3 +96,20 @@ jobs:
           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 -
+
+
+      - uses: actions/github-script@v6
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            github.rest.issues.createComment({
+              issue_number: context.issue.number,
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              body: '👋 Thanks for reporting!'
+            })