Fix 2 small formatting error of default value in options.md

[antoine2711]

There are 2 default values that don't have the proper formatting. This fixes those 2 small formatting error of default value in options.md.

Regards, Antoine

[niten94]

The changes were done in #2874 and #3576 too but this has been merged, so I think they may have been overlooked. But to be honest, I did not search old pull requests when I created #3576.

[JoeKar]

@niten94:
Ah, sorry...indeed it was overlooked.

[niten94]

No problem. New pull requests with similar changes could be opened, so I meant to just remind that they may be done already in #3576. I am sorry too that the pull request title is not clear, but I will change it when I get home or tomorrow.

[antoine2711]

No problem. New pull requests with similar changes could be opened, so I meant to just remind that they may be done already in #3576. I am sorry too that the pull request title is not clear, but I will change it when I get home or tomorrow.

Hi @niten94: would there have been a way for me to know it was already proposed in another pull request?

Regards, Antoine

[niten94]

These are the only ways that I know to check if a change has already been proposed in another pull request:

• Searching the filename or Go package (like buffer package in internal/buffer directory) where the change is done
• Searching words or synonyms describing the change
• Using a script that uses GitHub API and parses JSON result to display pull requests modifying file to be specified

Only seeing all pull requests with the proposed change cannot usually be done, so I think it is fine to not spend a lot of time trying to check.

[antoine2711]

• Searching the filename or Go package (like buffer package in internal/buffer directory) where the change is done

@niten94 :
I tried all these 4:

is:pr is:open /runtime/help/options.md
is:pr is:open options.md 
is:pr is:open path:/runtime/help/options.md
is:pr is:open path:/runtime/help/options.md * 

And this only finds my PR…

is:pr is:open pluginrepos 

And I couldn't even find my 2nd PR for another documentation bug (PR#3671)…
Can you guide me for the correct searching syntax?

Regards, Antoine

[niten94]

There is no syntax like is:pr that can be used to match pull requests where a file is modified. Pull requests where the name of the file modified is written in the title or description can be searched with is:pr is:open options.md like you have done, but I realized there are not much pull requests like that.

Thinking again about my comment,

• Using a script that uses GitHub API and parses JSON result to display pull requests modifying file to be specified

I checked now how this could be done but an API request that returns the list of files modified has to be made with each pull request too, so this was actually not a good idea.

• Searching words or synonyms describing the change

I think this is the only method usually done even though the results are not accurate. I would usually try searching more than once with combinations of these terms in the case of #3617 as an example: help, options, array, default, value, options.md, pluginrepos, pluginchannels

[antoine2711]

@niten94 : thanks again for taking the time to answer me.

And if your feels my contribution in [#3617] is good, don't hesitate to merge it.

Actually, if one does: micro -options, they'll get it:

(…)
-pluginchannels value
    	Default value: '[https://raw.githubusercontent.com/micro-editor/plugin-channel/master/channel.json]'
-pluginrepos value
    	Default value: '[]'
(…)

Regards, Antoine