You've already forked library-registry
mirror of
https://github.com/arduino/library-registry.git
synced 2025-07-01 12:01:41 +03:00
Merge pull request #36 from per1234/rename-registry
Use unique name for index source file
This commit is contained in:
2
.github/workflows/manage-prs.yml
vendored
2
.github/workflows/manage-prs.yml
vendored
@ -360,7 +360,7 @@ jobs:
|
||||
|
||||
- name: Add index source file entry for submissions
|
||||
run: |
|
||||
INDEX_SOURCE_FILE_PATH="${{ github.workspace }}/repositories.txt"
|
||||
INDEX_SOURCE_FILE_PATH="${{ github.workspace }}/registry.txt"
|
||||
git config --global user.email "bot@arduino.cc"
|
||||
git config --global user.name "ArduinoBot"
|
||||
echo "${{ needs.parse.outputs.index-entry }}" >> "$INDEX_SOURCE_FILE_PATH"
|
||||
|
Reference in New Issue
Block a user