zyedidia/micro
1
Fork 0
mirror of https://github.com/zyedidia/micro.git synced 2025-06-18 14:55:38 -04:00
Code Issues Actions 1 Packages Projects Releases Wiki Activity

Merge 03e9ab593e into 91832d0016

Browse Source
This commit is contained in:
Antoine Beaubien 2025-05-07 19:10:20 +02:00 committed by GitHub
commit 2453e3a00f
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
runtime/help/options.md
View File

@ -318,11 +318,11 @@ Here are the available options:
By default, this option points to the official plugin channel hosted on GitHub
at https://github.com/micro-editor/plugin-channel.
default value: `https://raw.githubusercontent.com/micro-editor/plugin-channel/master/channel.json`
default value: `[https://raw.githubusercontent.com/micro-editor/plugin-channel/master/channel.json]`
* `pluginrepos`: a list of links to plugin repositories.
default value: ``
default value: `[]`
* `readonly`: when enabled, disallows edits to the buffer. It is recommended
to only ever set this option locally using `setlocal`.