diff --git a/external/dev-ocean b/external/dev-ocean
index 90d07bfa..4b0f01f2 160000
--- a/external/dev-ocean
+++ b/external/dev-ocean
@@ -1 +1 @@
-Subproject commit 90d07bfa55df97951835545c188c38bc46682048
+Subproject commit 4b0f01f217ddb30cb768879de7dad15bbf7f07a8