diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-06-01 13:29:46 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-01 13:29:46 +0200 |
| commit | 6c1d71edc4a41c9ad89922fc433e617a813e4658 (patch) | |
| tree | d6322d1f3eaaeb38d9e9e5f44bd30528fd29e03f /doc/tools/makemd.py | |
| parent | 1820f9752dd258f81d18e2940a9a9d1c13216985 (diff) | |
| parent | 33909723735261991acccb6f1d3756e3659533d9 (diff) | |
Merge pull request #19280 from clktmr/master
Add cli paramerter --check-only for script parsing
Diffstat (limited to 'doc/tools/makemd.py')
0 files changed, 0 insertions, 0 deletions