Closed gamemaker1 closed 2 years ago
This is interesting. However, I worry about security issues if we add any plugin to the repo. We don't want any malicious plugins, and it is hard/impossible to automatically determine if a plugin is malicious. Perhaps this could be used as a tool for users to discover plugins on GitHub, although perhaps we should just recommend that plugin authors use the micro-editor-plugin
github tag for discoverability.
At the moment I think the plugin channel serves two uses:
This approach might be useful for automating the second usecase, and then users themselves determine if they want to manually install plugins from github. Perhaps there could be a tool/command integrated into micro (or separately) that searches github for plugins with a repo.json and a micro-editor-plugin
tag. It could additionally search according to some keywords that the user gives, and return results with some sort of ranking (stars/downloads/commits, something like that).
We don't want any malicious plugins, and it is hard/impossible to automatically determine if a plugin is malicious
Good point.
Perhaps there could be a tool/command integrated into micro (or separately) that searches github for plugins with a repo.json and a micro-editor-plugin tag. It could additionally search according to some keywords that the user gives, and return results with some sort of ranking (stars/downloads/commits, something like that).
I really like this idea - making something like a 'search engine' for micro plugins. Maybe I could give that a try.
Thanks again for your amazing work on Micro!
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.