diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 53648fdc2581a4d79760bf124d570b7692157ba8..0000000000000000000000000000000000000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "ci"] - path = ci - url = https://gitlab.mpi-sws.org/FP/iris-ci.git