Automate adding plugins to the channel #82
Closed
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi @zyedidia,
Thanks a ton for creating and maintaining Micro - it is an amazing project, and I use the editor for everything to do with, well... editing :D
I noticed that there are a lot of PRs for adding a plugin piling up - and I decided to help out by attempting to automate the process:
What this PR does
This PR makes the process of adding plugins to the channel automatic. It runs a script every 24 hours (via GitHub actions) that:
micro-editor-plugin
tag.repo.json
file in the root of the repository.repo.json
file.plugins.md
file.repo.json
file to thechannel.json
file.Caveats
A couple of issues:
1. Github-API dependent
This script only queries the GitHub API. So projects on Gitlab, Gitea, etc. cannot be added.
2. Cannot add plugins manually
This script overrides the current
channel.json
file every time it runs. This is so that we do not need to worry about repo/plugin renames, deletions and modifications to metadata. The downside is that if the repo owner does not add themicro-editor-plugin
tag, the plugin will not be listed. Also, if the repo is not on GitHub, the plugin will not be listed.I am working on a solution for the second caveat - so we can add plugins even if they are not on GitHub, or if the owner cannot add the
micro-editor-plugin
tag.