From 13c0316b06ed88cee46dded006f8bab05cdb1c42 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 18 Sep 2018 12:15:33 +0200 Subject: [PATCH] WIP CI --- ci | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ci b/ci index 7788488e..0a8b2f3f 160000 --- a/ci +++ b/ci @@ -1 +1 @@ -Subproject commit 7788488eacc707ea3fc1bcdba5284f52e9a201c4 +Subproject commit 0a8b2f3f15de414a3cbd365e6e4d54466f004e9d -- GitLab