diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-01 15:17:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-01 19:43:47 +0200 |
| commit | 75b2e9859d569d2868299c8c07d0262c88cdcc85 (patch) | |
| tree | e5f487408a98c3cd9afb629904149faef06e826d /test-suite/Makefile | |
| parent | 6b9b86ccd9f122e684cf4830f3e00bc3f70a0d8a (diff) | |
Updating to the new use of 3 universes, after Hurkens is simplified.
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 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" |