This repository was archived by the owner on Apr 26, 2026. It is now read-only.
File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 9393 echo "No changes to publish."
9494 fi
9595
96+ - name : Comment on PR with changed docs files
97+ if : github.event_name == 'pull_re echo "Using token from: ${{ steps.select_token.outputs.source }}"
98+
9699 - name : Comment on PR with changed docs files
97100 if : github.event_name == 'pull_request' && steps.docs_files.outputs.docs_files != '[]'
98101 env :
@@ -116,7 +119,7 @@ jobs:
116119
117120 - name : Post final publish comment
118121 env :
119- GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
122+ GITHUB_TOKEN : ${{ steps.select_token.outputs.token }}
120123 DOCS_FILES : ${{ steps.docs_files.outputs.docs_files }}
121124 run : |
122125 owner=$(echo "$GITHUB_REPOSITORY" | cut -d'/' -f1)
Original file line number Diff line number Diff line change 1+ .crush /
2+ CRUSH.md
Original file line number Diff line number Diff line change @@ -152,7 +152,7 @@ async function main() {
152152 await copyMarkdownRecursive ( docsDir , workingDir ) ;
153153
154154 // commit & push
155- exec ( `git -C "${ tempBase } " add --all` ) ;
155+ exec ( `git -C "${ workingDir } " add --all` ) ;
156156 const status = execSync ( `git -C "${ workingDir } " status --porcelain` ) . toString ( ) . trim ( ) ;
157157 if ( ! status ) {
158158 console . log ( 'No changes to commit.' ) ;
You can’t perform that action at this time.
0 commit comments