diff options
| -rw-r--r-- | tools/git-reindent-branch.py (renamed from git-reindent-branch.py) | 0 | ||||
| -rw-r--r-- | tools/indent.py (renamed from indent.py) | 0 | ||||
| -rw-r--r-- | tools/render_md.py (renamed from render_md.py) | 0 |
3 files changed, 0 insertions, 0 deletions
diff --git a/git-reindent-branch.py b/tools/git-reindent-branch.py index c207f5946f..c207f5946f 100644 --- a/git-reindent-branch.py +++ b/tools/git-reindent-branch.py diff --git a/indent.py b/tools/indent.py index 560c13c77d..560c13c77d 100644 --- a/indent.py +++ b/tools/indent.py diff --git a/render_md.py b/tools/render_md.py index 16c4bbe8a3..16c4bbe8a3 100644 --- a/render_md.py +++ b/tools/render_md.py |