diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-10-02 12:27:49 +0200 |
|---|---|---|
| committer | Rémi Verschelde <rverschelde@gmail.com> | 2018-10-02 12:28:08 +0200 |
| commit | 0cc3aff8edd5f63436814a6b2219044d94eb8201 (patch) | |
| tree | 400838f5bb5bdc861d925cafa81543281ffe3d2f /editor/editor_path.h | |
| parent | 106acb27f914681e9172e23d83dd394205259ea5 (diff) | |
doc: Drop obsolete makemd.py, dates back to GitHub Wiki days
It has not been kept in sync with makerst.py, so it does not serve
much purpose nowadays.
Diffstat (limited to 'editor/editor_path.h')
0 files changed, 0 insertions, 0 deletions