diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-10-09 14:52:11 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-09 14:52:11 +0200 |
| commit | cbeeba9c0346517801a7610154cd85955d542919 (patch) | |
| tree | 79f68381b08cc0576b56a4e97bc3ad3238d08706 /editor | |
| parent | 8ddbd1977793ef1318d3557001310c59277321d0 (diff) | |
| parent | b772f5adc9bd9384994bdf60ac4d0285c47bc3e2 (diff) | |
Merge pull request #11908 from mhilbrunner/docstatus-flagerror
doc_status.py: Error message for unknown CLI flag, shebang change
[ci skip]
Diffstat (limited to 'editor')
0 files changed, 0 insertions, 0 deletions