aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5188fe6c5..8bb9210b6 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -376,7 +376,7 @@ misc/deps-order.log:
} > "$@"
# Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 4
+EXPECTED_UNIVERSES := 3
universes: misc/universes.log
misc/universes.log: misc/universes/all_stdlib.v
@echo "TEST misc/universes"