diff options
| author | Emilio Jesus Gallego Arias | 2019-10-31 20:41:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 20:41:30 +0100 |
| commit | 151b84a3540d1972d53460780396f2749d0378cf (patch) | |
| tree | 42a1d2b0784d83f489dc043f57cf9482056ab501 /plugins/syntax/plugin_base.dune | |
| parent | bc70919118fe5450c3bb798632d64823659f4814 (diff) | |
| parent | 85905b38c15c3d2bb73e878e6e7db180b73d468e (diff) | |
Merge PR #10985: Print argument info as an Arguments command in About
Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions