arduino/library-registry
1
0
Fork 0
mirror of https://github.com/arduino/library-registry.git synced 2025-07-02 23:02:27 +03:00
Code Activity

Use unique name for index source file

Browse Source 
Previously, the submission list and the Library Manager index source list were both named "repositories.txt". I found having two files with similar content, but different purposes makes the already complex system unnecessarily difficult to understand.

Unlike the index source list, the submission list is solely a list of repositories, so its current "repositories.txt"
name is appropriate. The index source list contains other information unrelated to the library repository, so the
"repositories.txt" name is not so appropriate. Since the repository is named "library-registry", the filename
"registry.txt" makes sense.
This commit is contained in:
per1234
2021-05-24 21:14:49 -07:00
parent 123186a5b9
commit 8ccb23ac21
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/manage-prs.yml vendored
View File

@ -360,7 +360,7 @@ jobs:
- name: Add index source file entry for submissions - name: Add index source file entry for submissions
run: | 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.email "bot@arduino.cc"
git config --global user.name "ArduinoBot" git config --global user.name "ArduinoBot"
echo "${{ needs.parse.outputs.index-entry }}" >> "$INDEX_SOURCE_FILE_PATH" echo "${{ needs.parse.outputs.index-entry }}" >> "$INDEX_SOURCE_FILE_PATH"