github/zyedidia.micro
2
0
Fork 0
mirror of https://github.com/zyedidia/micro.git synced 2026-03-22 08:47:15 +09:00
Code Issues Packages Projects Releases Wiki Activity

Minor fix for comment plugin and migrating to use "comment.type" option (#3424)

Browse Source 
Fixing comment plugin not using user settings when overriding default
setting,
Migrating comment plugin to use "comment.type" option instead
This commit is contained in:
Neko Box Coder
2025-06-24 21:30:26 +01:00
committed by GitHub
parent 97b5e3506e
commit 4db233acf4
2 changed files with 28 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
runtime/plugins/comment/help/comment.md
View File

@@ -80,10 +80,10 @@ but it is only available for certain filetypes:
* zsh: `# %s`
If your filetype is not available here, you can simply modify
the `commenttype` option:
the `comment.type` option:
```
set commenttype "/* %s */"
set comment.type "/* %s */"
```
Or in your `settings.json`:
@@ -91,7 +91,12 @@ Or in your `settings.json`:
```json
{
"*.c": {
"commenttype": "/* %s */"
"comment.type": "/* %s */"
}
}
```
`commenttype` (without the dot) is the legacy option that is
superseded by `comment.type`. `commenttype` is still supported
but deprecated.
**Use `comment.type` instead.**