From 96191ed7ef792478c86890a0ebdbbbea0dc9c9ab Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 20 May 2021 14:06:35 +0200 Subject: [PATCH] remove ancient submodule leftovers --- .gitmodules | 3 --- 1 file changed, 3 deletions(-) delete mode 100644 .gitmodules diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 53648fdc2..000000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "ci"] - path = ci - url = https://gitlab.mpi-sws.org/FP/iris-ci.git -- GitLab