diff --git a/external/dev-ocean b/external/dev-ocean index 1a82c696..3865e190 160000 --- a/external/dev-ocean +++ b/external/dev-ocean @@ -1 +1 @@ -Subproject commit 1a82c6964075aa6358643cc902f971e64da32b72 +Subproject commit 3865e1905c1309970359adb5e984fa7e0e49b5cb