diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:07:32 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:07:32 +0530 |
| commit | 5e5d51762df0e34769225e8c59c77b97b1212c29 (patch) | |
| tree | 61aa0a74d77089ed4a7db12ff6fc46059ab2fb61 /test-suite/Makefile | |
| parent | 9d8347abc07dec1edd804b2fa39db40088b5cf3d (diff) | |
There was one more universe needed due to the use of now non-universe-polymorphic
ID, fixing the script results in 3 universes for the stdlib again.
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 055485d0b..4a3a287c0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -387,7 +387,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" |