diff --git a/external/dev-ocean b/external/dev-ocean index 947a1a71..95831642 160000 --- a/external/dev-ocean +++ b/external/dev-ocean @@ -1 +1 @@ -Subproject commit 947a1a71e31698bb2dd0be5ae1f5c78bc3dc7b8f +Subproject commit 958316426a441f34d05a2240806577008713b5a7