From 5c8595d64c361cdd9d18dca5ab769aaf109d625d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 12 May 2019 20:19:43 +0200 Subject: [PATCH] remove dead submodule --- .gitmodules | 3 --- 1 file changed, 3 deletions(-) delete mode 100644 .gitmodules diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 53648fdc..00000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "ci"] - path = ci - url = https://gitlab.mpi-sws.org/FP/iris-ci.git -- GitLab