From 9428d768df322e54b1744cac2a01f6f25751e319 Mon Sep 17 00:00:00 2001
From: tobiasKaminsky <tobias@kaminsky.me>
Date: Mon, 2 Oct 2017 11:13:42 +0200
Subject: [PATCH] remove git submodule

---
 .gitmodules       | 0
 user_manual/ocdoc | 1 -
 2 files changed, 1 deletion(-)
 create mode 100644 .gitmodules
 delete mode 160000 user_manual/ocdoc

diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/user_manual/ocdoc b/user_manual/ocdoc
deleted file mode 160000
index 343496c792..0000000000
--- a/user_manual/ocdoc
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 343496c792616459e8204b6614fd42a1b16a6d68