aboutsummaryrefslogtreecommitdiff
path: root/engine/univNames.mli
diff options
context:
space:
mode:
authorMaxime Dénès2018-12-04 10:33:47 +0100
committerMaxime Dénès2018-12-06 11:09:27 +0100
commit3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 (patch)
tree6ea705714c862ab019aa312daf42d40ca50a4ace /engine/univNames.mli
parenta2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (diff)
Fix race condition triggered by fresh universe generation
Remote counters were trying to build universe levels (as opposed to simple integers), but did not have access to the right dirpath at construction time. We fix it by constructing the level only at use time, and we introduce some abstractions for qualified and unqualified level names.
Diffstat (limited to 'engine/univNames.mli')
0 files changed, 0 insertions, 0 deletions