diff --git a/external/dev-ocean b/external/dev-ocean index 96e18f52..17d9bbaf 160000 --- a/external/dev-ocean +++ b/external/dev-ocean @@ -1 +1 @@ -Subproject commit 96e18f52dca83264b53348387c295376d6b25adb +Subproject commit 17d9bbaffa0dcb29fc2e01794723c245f6f4a57d