From a358a355e4e9ec406d9c57e890a90e2d367377be Mon Sep 17 00:00:00 2001
From: Andreas Zweili <andreas@2li.ch>
Date: Tue, 27 Feb 2018 20:28:38 +0100
Subject: [PATCH] remove an unneeded file

---
 docs/doku.synctex(busy) | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 delete mode 100644 docs/doku.synctex(busy)

diff --git a/docs/doku.synctex(busy) b/docs/doku.synctex(busy)
deleted file mode 100644
index e69de29..0000000