tools: Add git diff.

- This is worth it afterall.
- Eris will get out of sync when the diffs are commited,
  but this is also true of git-blame and git-log.
- The user can refresh the old results with shift-r.
This commit is contained in:
Andrew Hamilton 2021-07-11 16:25:25 +10:00
parent c5efd3a74b
commit 071096821c
4 changed files with 14 additions and 5 deletions

View file

@ -7,7 +7,7 @@ import eris.tools as tools
def main():
all_tools = ([(["*"], tools.generic_tools() +
[tools.git_blame, tools.git_log])] +
[tools.git_diff, tools.git_blame, tools.git_log])] +
tools.TOOLS_FOR_EXTENSIONS)
tool_set = set()
extension_set = set()