From 911221e9c10c13847694f5fd2be646d4a6b4cc92 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 12 May 2019 20:19:15 +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