diff --git a/extern/mops b/extern/mops index 9621fdd0..3a2847c1 160000 --- a/extern/mops +++ b/extern/mops @@ -1 +1 @@ -Subproject commit 9621fdd0d8e49cea05a17d830a4e57fcfbf66b88 +Subproject commit 3a2847c160ea54abc2280208fdc8d57c025a42de