From 8e45f78d462f8817fbfece8cb96c7be5d008bb03 Mon Sep 17 00:00:00 2001 From: Matthias Kretschmann <m@kretschmann.io> Date: Thu, 22 Nov 2018 15:53:22 +0100 Subject: [PATCH] bump dev-ocean --- external/dev-ocean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/external/dev-ocean b/external/dev-ocean index 088cfe2a..cbdb96cf 160000 --- a/external/dev-ocean +++ b/external/dev-ocean @@ -1 +1 @@ -Subproject commit 088cfe2ae2eed4f3c676d0a9afdf30f69b705d79 +Subproject commit cbdb96cf4d8e1f98a79b82db00f57dc0691b2b3d