diff --git a/external/dev-ocean b/external/dev-ocean index 0aeaf4ee..dfaf26f5 160000 --- a/external/dev-ocean +++ b/external/dev-ocean @@ -1 +1 @@ -Subproject commit 0aeaf4eeadda2901da629ead14748c89d05c26dc +Subproject commit dfaf26f53366130da2973a25e596f0ed6fe7b0c7