From fb2b3591aa832dce5d8d9295d444fbe3909980de Mon Sep 17 00:00:00 2001
From: Johannes Ranke <jranke@uni-bremen.de>
Date: Fri, 12 May 2023 17:11:08 +0200
Subject: Clean out unused stuff

---
 bin/git_diff | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100755 bin/git_diff

(limited to 'bin/git_diff')

diff --git a/bin/git_diff b/bin/git_diff
deleted file mode 100755
index a35fc68..0000000
--- a/bin/git_diff
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/bin/bash
-# un-comment one diff tool you'd like to use
-#
-# From https://stackoverflow.com/a/7669988/3805440, thanks
-
-# side-by-side diff with custom options:
-/usr/bin/sdiff -w200 -l "$2" "$5" 
-
-# using kdiff3 as the side-by-side diff:
-#/usr/bin/kdiff3 "$2" "$5"
-
-# using Meld 
-#/usr/bin/meld "$2" "$5"
-
-# using VIM
-#/usr/bin/nvim -d "$2" "$5"
-- 
cgit v1.2.1