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